perm filename BOYER.TIM[TIM,LSP]5 blob
sn#727370 filedate 1983-10-18 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00017 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00003 00002 Comparison of LISPS
C00005 00003 The ELISP code
C00026 00004 (FILECREATED " 5-Jul-82 12:52:49" <CL.BOYER.LISPS>IREWRITE..4 14918
C00051 00005 The Maclisp Code
C00072 00006 The ELISP test
C00073 00007 Interlisp bcompl blocklib swap and noswap
C00076 00008 Interlisp bcompl no blocklib swap and noswap
C00080 00009 Maclisp
C00086 00010 Interlisp (Dolphin and Dorado)
C00117 00011 The INTERLISP VAX test
C00120 00012 SAIL
C00122 00013 SAIL (FIXSW T)
C00124 00014 Boyer
C00125 00015 NIL
C00127 00016 FRANZ
C00137 00017 SCORE Oct 18, 1983
C00139 ENDMK
C⊗;
Comparison of LISPS
This page contains a summary. Subsequent pages contain the
code used and documentation of the tests. All the code was compiled.
Non GC time (seconds) GC time Total
MACLISP (2060) 8.5 5.3 13.8
UCILISP (2060, (nouuo nil)) 9.3 4.7 14
INTERLISP (bcompl, blklib, swap, 2060) 11 6 17
ELISP (2060) 11 7 18
INTERLISP (bcompl, blklib, noswap, 2060) 11 7.5 18.5
INTERLISP (Dorado, bcompl, blklib) 18 11 29
INTERLISP (bcompl, no blklib, noswap, 2060) 39 7 46
INTERLISP (bcompl, no blklib, swap, 2060) 64 6 70
INTERLISP (VAX-780) 80 3 83
ZETALISP (LM-2, 1meg, gc-on) breakdown not available 97
INTERLISP (Dolphin, 1meg, bcompl, blklib) 132 35 167
The ELISP code
(DECLARE (SPECIAL UNIFY-SUBST TEMP-TEMP))
(DE ADD-LEMMA (TERM)
(COND ((AND (NOT (ATOM TERM))
(EQ (CAR TERM)
(QUOTE EQUAL))
(NOT (ATOM (CADR TERM))))
(PUTPROP (CAR (CADR TERM))
(CONS TERM (GET (CAR (CADR TERM))
(QUOTE LEMMAS)))
(QUOTE LEMMAS)))
(T (ERROR (LIST (QUOTE ADD-LEMMA-DID-NOT-LIKE-TERM) TERM)
))))
(DE ADD-LEMMA-LST (LST)
(COND ((NULL LST)
T)
(T (ADD-LEMMA (CAR LST))
(ADD-LEMMA-LST (CDR LST)))))
(DE APPLY-SUBST (ALIST TERM)
(COND ((ATOM TERM)
(COND ((SETQ TEMP-TEMP (ASSOC TERM ALIST))
(CDR TEMP-TEMP))
(T TERM)))
(T (CONS (CAR TERM)
(APPLY-SUBST-LST ALIST (CDR TERM))))))
(DE APPLY-SUBST-LST (ALIST LST)
(COND ((NULL LST)
NIL)
(T (CONS (APPLY-SUBST ALIST (CAR LST))
(APPLY-SUBST-LST ALIST (CDR LST))))))
(DE FALSEP (X LST)
(OR (EQUAL X (QUOTE (F)))
(MEMBER X LST)))
(DE ONE-WAY-UNIFY (TERM1 TERM2)
(PROGN (SETQ UNIFY-SUBST NIL)
(ONE-WAY-UNIFY1 TERM1 TERM2)))
(DE ONE-WAY-UNIFY1 (TERM1 TERM2)
(COND ((ATOM TERM2)
(COND ((SETQ TEMP-TEMP (ASSOC TERM2 UNIFY-SUBST))
(EQUAL TERM1 (CDR TEMP-TEMP)))
(T (SETQ UNIFY-SUBST (CONS (CONS TERM2 TERM1)
UNIFY-SUBST))
T)))
((ATOM TERM1)
NIL)
((EQ (CAR TERM1)
(CAR TERM2))
(ONE-WAY-UNIFY1-LST (CDR TERM1)
(CDR TERM2)))
(T NIL)))
(DE ONE-WAY-UNIFY1-LST (LST1 LST2)
(COND ((NULL LST1)
T)
((ONE-WAY-UNIFY1 (CAR LST1)
(CAR LST2))
(ONE-WAY-UNIFY1-LST (CDR LST1)
(CDR LST2)))
(T NIL)))
(DE REWRITE (TERM)
(COND ((ATOM TERM)
TERM)
(T (REWRITE-WITH-LEMMAS (CONS (CAR TERM)
(REWRITE-ARGS (CDR TERM)))
(GET (CAR TERM)
(QUOTE LEMMAS))))))
(DE REWRITE-ARGS (LST)
(COND ((NULL LST)
NIL)
(T (CONS (REWRITE (CAR LST))
(REWRITE-ARGS (CDR LST))))))
(DE REWRITE-WITH-LEMMAS (TERM LST)
(COND ((NULL LST)
TERM)
((ONE-WAY-UNIFY TERM (CADR (CAR LST)))
(REWRITE (APPLY-SUBST UNIFY-SUBST (CADDR (CAR LST)))))
(T (REWRITE-WITH-LEMMAS TERM (CDR LST)))))
(DE
SETUP NIL
(ADD-LEMMA-LST
(QUOTE ((EQUAL (COMPILE FORM)
(REVERSE (CODEGEN (OPTIMIZE FORM)
(NIL))))
(EQUAL (EQP X Y)
(EQUAL (FIX X)
(FIX Y)))
(EQUAL (GREATERP X Y)
(LESSP Y X))
(EQUAL (LESSEQP X Y)
(NOT (LESSP Y X)))
(EQUAL (GREATEREQP X Y)
(NOT (LESSP X Y)))
(EQUAL (BOOLEAN X)
(OR (EQUAL X (T))
(EQUAL X (F))))
(EQUAL (IFF X Y)
(AND (IMPLIES X Y)
(IMPLIES Y X)))
(EQUAL (EVEN1 X)
(IF (ZEROP X)
(T)
(ODD (SUB1 X))))
(EQUAL (COUNTPS- L PRED)
(COUNTPS-LOOP L PRED (ZERO)))
(EQUAL (FACT- I)
(FACT-LOOP I 1))
(EQUAL (REVERSE- X)
(REVERSE-LOOP X (NIL)))
(EQUAL (DIVIDES X Y)
(ZEROP (REMAINDER Y X)))
(EQUAL (ASSUME-TRUE VAR ALIST)
(CONS (CONS VAR (T))
ALIST))
(EQUAL (ASSUME-FALSE VAR ALIST)
(CONS (CONS VAR (F))
ALIST))
(EQUAL (TAUTOLOGY-CHECKER X)
(TAUTOLOGYP (NORMALIZE X)
(NIL)))
(EQUAL (FALSIFY X)
(FALSIFY1 (NORMALIZE X)
(NIL)))
(EQUAL (PRIME X)
(AND (NOT (ZEROP X))
(NOT (EQUAL X (ADD1 (ZERO))))
(PRIME1 X (SUB1 X))))
(EQUAL (AND P Q)
(IF P (IF Q (T)
(F))
(F)))
(EQUAL (OR P Q)
(IF P (T)
(IF Q (T)
(F))
(F)))
(EQUAL (NOT P)
(IF P (F)
(T)))
(EQUAL (IMPLIES P Q)
(IF P (IF Q (T)
(F))
(T)))
(EQUAL (FIX X)
(IF (NUMBERP X)
X
(ZERO)))
(EQUAL (IF (IF A B C)
D E)
(IF A (IF B D E)
(IF C D E)))
(EQUAL (ZEROP X)
(OR (EQUAL X (ZERO))
(NOT (NUMBERP X))))
(EQUAL (PLUS (PLUS X Y)
Z)
(PLUS X (PLUS Y Z)))
(EQUAL (EQUAL (PLUS A B)
(ZERO))
(AND (ZEROP A)
(ZEROP B)))
(EQUAL (DIFFERENCE X X)
(ZERO))
(EQUAL (EQUAL (PLUS A B)
(PLUS A C))
(EQUAL (FIX B)
(FIX C)))
(EQUAL (EQUAL (ZERO)
(DIFFERENCE X Y))
(NOT (LESSP Y X)))
(EQUAL (EQUAL X (DIFFERENCE X Y))
(AND (NUMBERP X)
(OR (EQUAL X (ZERO))
(ZEROP Y))))
(EQUAL (MEANING (PLUS-TREE (APPEND X Y))
A)
(PLUS (MEANING (PLUS-TREE X)
A)
(MEANING (PLUS-TREE Y)
A)))
(EQUAL (MEANING (PLUS-TREE (PLUS-FRINGE X))
A)
(FIX (MEANING X A)))
(EQUAL (APPEND (APPEND X Y)
Z)
(APPEND X (APPEND Y Z)))
(EQUAL (REVERSE (APPEND A B))
(APPEND (REVERSE B)
(REVERSE A)))
(EQUAL (TIMES X (PLUS Y Z))
(PLUS (TIMES X Y)
(TIMES X Z)))
(EQUAL (TIMES (TIMES X Y)
Z)
(TIMES X (TIMES Y Z)))
(EQUAL (EQUAL (TIMES X Y)
(ZERO))
(OR (ZEROP X)
(ZEROP Y)))
(EQUAL (EXEC (APPEND X Y)
PDS ENVRN)
(EXEC Y (EXEC X PDS ENVRN)
ENVRN))
(EQUAL (MC-FLATTEN X Y)
(APPEND (FLATTEN X)
Y))
(EQUAL (MEMBER X (APPEND A B))
(OR (MEMBER X A)
(MEMBER X B)))
(EQUAL (MEMBER X (REVERSE Y))
(MEMBER X Y))
(EQUAL (LENGTH (REVERSE X))
(LENGTH X))
(EQUAL (MEMBER A (INTERSECT B C))
(AND (MEMBER A B)
(MEMBER A C)))
(EQUAL (NTH (ZERO)
I)
(ZERO))
(EQUAL (EXP I (PLUS J K))
(TIMES (EXP I J)
(EXP I K)))
(EQUAL (EXP I (TIMES J K))
(EXP (EXP I J)
K))
(EQUAL (REVERSE-LOOP X Y)
(APPEND (REVERSE X)
Y))
(EQUAL (REVERSE-LOOP X (NIL))
(REVERSE X))
(EQUAL (COUNT-LIST Z (SORT-LP X Y))
(PLUS (COUNT-LIST Z X)
(COUNT-LIST Z Y)))
(EQUAL (EQUAL (APPEND A B)
(APPEND A C))
(EQUAL B C))
(EQUAL (PLUS (REMAINDER X Y)
(TIMES Y (QUOTIENT X Y)))
(FIX X))
(EQUAL (POWER-EVAL (BIG-PLUS1 L I BASE)
BASE)
(PLUS (POWER-EVAL L BASE)
I))
(EQUAL (POWER-EVAL (BIG-PLUS X Y I BASE)
BASE)
(PLUS I (PLUS (POWER-EVAL X BASE)
(POWER-EVAL Y BASE))))
(EQUAL (REMAINDER Y 1)
(ZERO))
(EQUAL (LESSP (REMAINDER X Y)
Y)
(NOT (ZEROP Y)))
(EQUAL (REMAINDER X X)
(ZERO))
(EQUAL (LESSP (QUOTIENT I J)
I)
(AND (NOT (ZEROP I))
(OR (ZEROP J)
(NOT (EQUAL J 1)))))
(EQUAL (LESSP (REMAINDER X Y)
X)
(AND (NOT (ZEROP Y))
(NOT (ZEROP X))
(NOT (LESSP X Y))))
(EQUAL (POWER-EVAL (POWER-REP I BASE)
BASE)
(FIX I))
(EQUAL (POWER-EVAL (BIG-PLUS (POWER-REP I BASE)
(POWER-REP J BASE)
(ZERO)
BASE)
BASE)
(PLUS I J))
(EQUAL (GCD X Y)
(GCD Y X))
(EQUAL (NTH (APPEND A B)
I)
(APPEND (NTH A I)
(NTH B (DIFFERENCE I (LENGTH A)))))
(EQUAL (DIFFERENCE (PLUS X Y)
X)
(FIX Y))
(EQUAL (DIFFERENCE (PLUS Y X)
X)
(FIX Y))
(EQUAL (DIFFERENCE (PLUS X Y)
(PLUS X Z))
(DIFFERENCE Y Z))
(EQUAL (TIMES X (DIFFERENCE C W))
(DIFFERENCE (TIMES C X)
(TIMES W X)))
(EQUAL (REMAINDER (TIMES X Z)
Z)
(ZERO))
(EQUAL (DIFFERENCE (PLUS B (PLUS A C))
A)
(PLUS B C))
(EQUAL (DIFFERENCE (ADD1 (PLUS Y Z))
Z)
(ADD1 Y))
(EQUAL (LESSP (PLUS X Y)
(PLUS X Z))
(LESSP Y Z))
(EQUAL (LESSP (TIMES X Z)
(TIMES Y Z))
(AND (NOT (ZEROP Z))
(LESSP X Y)))
(EQUAL (LESSP Y (PLUS X Y))
(NOT (ZEROP X)))
(EQUAL (GCD (TIMES X Z)
(TIMES Y Z))
(TIMES Z (GCD X Y)))
(EQUAL (VALUE (NORMALIZE X)
A)
(VALUE X A))
(EQUAL (EQUAL (FLATTEN X)
(CONS Y (NIL)))
(AND (NLISTP X)
(EQUAL X Y)))
(EQUAL (LISTP (GOPHER X))
(LISTP X))
(EQUAL (SAMEFRINGE X Y)
(EQUAL (FLATTEN X)
(FLATTEN Y)))
(EQUAL (EQUAL (GREATEST-FACTOR X Y)
(ZERO))
(AND (OR (ZEROP Y)
(EQUAL Y 1))
(EQUAL X (ZERO))))
(EQUAL (EQUAL (GREATEST-FACTOR X Y)
1)
(EQUAL X 1))
(EQUAL (NUMBERP (GREATEST-FACTOR X Y))
(NOT (AND (OR (ZEROP Y)
(EQUAL Y 1))
(NOT (NUMBERP X)))))
(EQUAL (TIMES-LIST (APPEND X Y))
(TIMES (TIMES-LIST X)
(TIMES-LIST Y)))
(EQUAL (PRIME-LIST (APPEND X Y))
(AND (PRIME-LIST X)
(PRIME-LIST Y)))
(EQUAL (EQUAL Z (TIMES W Z))
(AND (NUMBERP Z)
(OR (EQUAL Z (ZERO))
(EQUAL W 1))))
(EQUAL (GREATEREQPR X Y)
(NOT (LESSP X Y)))
(EQUAL (EQUAL X (TIMES X Y))
(OR (EQUAL X (ZERO))
(AND (NUMBERP X)
(EQUAL Y 1))))
(EQUAL (REMAINDER (TIMES Y X)
Y)
(ZERO))
(EQUAL (EQUAL (TIMES A B)
1)
(AND (NOT (EQUAL A (ZERO)))
(NOT (EQUAL B (ZERO)))
(NUMBERP A)
(NUMBERP B)
(EQUAL (SUB1 A)
(ZERO))
(EQUAL (SUB1 B)
(ZERO))))
(EQUAL (LESSP (LENGTH (DELETE X L))
(LENGTH L))
(MEMBER X L))
(EQUAL (SORT2 (DELETE X L))
(DELETE X (SORT2 L)))
(EQUAL (DSORT X)
(SORT2 X))
(EQUAL (LENGTH (CONS X1
(CONS X2
(CONS X3 (CONS X4
(CONS X5
(CONS X6 X7)))))))
(PLUS 6 (LENGTH X7)))
(EQUAL (DIFFERENCE (ADD1 (ADD1 X))
2)
(FIX X))
(EQUAL (QUOTIENT (PLUS X (PLUS X Y))
2)
(PLUS X (QUOTIENT Y 2)))
(EQUAL (SIGMA (ZERO)
I)
(QUOTIENT (TIMES I (ADD1 I))
2))
(EQUAL (PLUS X (ADD1 Y))
(IF (NUMBERP Y)
(ADD1 (PLUS X Y))
(ADD1 X)))
(EQUAL (EQUAL (DIFFERENCE X Y)
(DIFFERENCE Z Y))
(IF (LESSP X Y)
(NOT (LESSP Y Z))
(IF (LESSP Z Y)
(NOT (LESSP Y X))
(EQUAL (FIX X)
(FIX Z)))))
(EQUAL (MEANING (PLUS-TREE (DELETE X Y))
A)
(IF (MEMBER X Y)
(DIFFERENCE (MEANING (PLUS-TREE Y)
A)
(MEANING X A))
(MEANING (PLUS-TREE Y)
A)))
(EQUAL (TIMES X (ADD1 Y))
(IF (NUMBERP Y)
(PLUS X (TIMES X Y))
(FIX X)))
(EQUAL (NTH (NIL)
I)
(IF (ZEROP I)
(NIL)
(ZERO)))
(EQUAL (LAST (APPEND A B))
(IF (LISTP B)
(LAST B)
(IF (LISTP A)
(CONS (CAR (LAST A))
B)
B)))
(EQUAL (EQUAL (LESSP X Y)
Z)
(IF (LESSP X Y)
(EQUAL T Z)
(EQUAL F Z)))
(EQUAL (ASSIGNMENT X (APPEND A B))
(IF (ASSIGNEDP X A)
(ASSIGNMENT X A)
(ASSIGNMENT X B)))
(EQUAL (CAR (GOPHER X))
(IF (LISTP X)
(CAR (FLATTEN X))
(ZERO)))
(EQUAL (FLATTEN (CDR (GOPHER X)))
(IF (LISTP X)
(CDR (FLATTEN X))
(CONS (ZERO)
(NIL))))
(EQUAL (QUOTIENT (TIMES Y X)
Y)
(IF (ZEROP Y)
(ZERO)
(FIX X)))
(EQUAL (GET J (SET I VAL MEM))
(IF (EQP J I)
VAL
(GET J MEM)))))))
(DE TAUTOLOGYP (X TRUE-LST FALSE-LST)
(COND ((TRUEP X TRUE-LST)
T)
((FALSEP X FALSE-LST)
NIL)
((ATOM X)
NIL)
((EQ (CAR X)
(QUOTE IF))
(COND ((TRUEP (CADR X)
TRUE-LST)
(TAUTOLOGYP (CADDR X)
TRUE-LST FALSE-LST))
((FALSEP (CADR X)
FALSE-LST)
(TAUTOLOGYP (CADDDR X)
TRUE-LST FALSE-LST))
(T (AND (TAUTOLOGYP (CADDR X)
(CONS (CADR X)
TRUE-LST)
FALSE-LST)
(TAUTOLOGYP (CADDDR X)
TRUE-LST
(CONS (CADR X)
FALSE-LST))))))
(T NIL)))
(DE TAUTP (X)
(TAUTOLOGYP (REWRITE X)
NIL NIL))
(DE TEST NIL
(TIMER (TEST1)))
(DE TEST1 NIL
(PROG (TERM ANS)
(SETQ TERM
(APPLY-SUBST
(QUOTE ((X F (PLUS (PLUS A B)
(PLUS C (ZERO))))
(Y F (TIMES (TIMES A B)
(PLUS C D)))
(Z F (REVERSE (APPEND (APPEND A B)
(NIL))))
(U EQUAL (PLUS A B)
(DIFFERENCE X Y))
(W LESSP (REMAINDER A B)
(MEMBER A (LENGTH B)))))
(QUOTE (IMPLIES (AND (IMPLIES X Y)
(AND (IMPLIES Y Z)
(AND (IMPLIES Z U)
(IMPLIES U W))))
(IMPLIES X W)))))
(SETQ ANS (TAUTP TERM))
(RETURN (LIST ANS))))
(DE TRANS-OF-IMPLIES (N)
(LIST (QUOTE IMPLIES)
(TRANS-OF-IMPLIES1 N)
(LIST (QUOTE IMPLIES)
0 N)))
(DE TRANS-OF-IMPLIES1 (N)
(COND ((EQUAL N 1)
(LIST (QUOTE IMPLIES)
0 1))
(T (LIST (QUOTE AND)
(LIST (QUOTE IMPLIES)
(SUB1 N)
N)
(TRANS-OF-IMPLIES1 (SUB1 N))))))
(DE TRUEP (X LST)
(OR (EQUAL X (QUOTE (T)))
(MEMBER X LST)))
(FILECREATED " 5-Jul-82 12:52:49" <CL.BOYER.LISPS>IREWRITE..4 14918
changes to: IREWRITECOMS
previous date: " 5-Jul-82 12:11:22" <CL.BOYER.LISPS>IREWRITE..3)
(PRETTYCOMPRINT IREWRITECOMS)
(RPAQQ IREWRITECOMS ((FNS * IREWRITEFNS)
(PROP BLKLIBRARYDEF MEMBER)
(BLOCKS (REWRITEBLOCK ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST
APPLY-SUBST-LST FALSEP ONE-WAY-UNIFY
ONE-WAY-UNIFY1 ONE-WAY-UNIFY1-LST PTIME
REWRITE REWRITE-ARGS REWRITE-WITH-LEMMAS
SETUP TAUTOLOGYP TAUTP TEST
TRANS-OF-IMPLIES TRANS-OF-IMPLIES1 TRUEP
(ENTRIES TEST SETUP)
(BLKLIBRARY EQUAL MEMBER GETPROP)
(GLOBALVARS TEMP-TEMP UNIFY-SUBST)))))
(RPAQQ IREWRITEFNS (ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST APPLY-SUBST-LST
FALSEP ONE-WAY-UNIFY ONE-WAY-UNIFY1
ONE-WAY-UNIFY1-LST PTIME REWRITE
REWRITE-ARGS REWRITE-WITH-LEMMAS SETUP
TAUTOLOGYP TAUTP TEST TRANS-OF-IMPLIES
TRANS-OF-IMPLIES1 TRUEP))
(DEFINEQ
(ADD-LEMMA
(LAMBDA (TERM)
(COND
((AND (NOT (ATOM TERM))
(EQ (CAR TERM)
(QUOTE EQUAL))
(NOT (ATOM (CADR TERM))))
(COND
((GETPROP (CAR (CADR TERM))
(QUOTE LEMMAS))
(PUTPROP (CAR (CADR TERM))
(QUOTE LEMMAS)
(CONS TERM (GETPROP (CAR (CADR TERM))
(QUOTE LEMMAS)))))
(T (SETPROPLIST (CAR (CADR TERM))
(CONS (QUOTE LEMMAS)
(CONS (LIST TERM)
(GETPROPLIST (CAR (CADR TERM))))))
)))
(T (ERROR (QUOTE ADD-LEMMA-DID-NOT-LIKE-TERM)
TERM)))))
(ADD-LEMMA-LST
(LAMBDA (LST)
(COND
((NULL LST)
T)
(T (ADD-LEMMA (CAR LST))
(ADD-LEMMA-LST (CDR LST))))))
(APPLY-SUBST
(LAMBDA (ALIST TERM)
(COND
((NLISTP TERM)
(COND
((SETQ TEMP-TEMP (FASSOC TERM ALIST))
(CDR TEMP-TEMP))
(T TERM)))
(T (CONS (CAR TERM)
(APPLY-SUBST-LST ALIST (CDR TERM)))))))
(APPLY-SUBST-LST
(LAMBDA (ALIST LST)
(COND
((NULL LST)
NIL)
(T (CONS (APPLY-SUBST ALIST (CAR LST))
(APPLY-SUBST-LST ALIST (CDR LST)))))))
(FALSEP
(LAMBDA (X LST)
(OR (EQUAL X (QUOTE (F)))
(MEMBER X LST))))
(ONE-WAY-UNIFY
(LAMBDA (TERM1 TERM2)
(PROGN (SETQ UNIFY-SUBST NIL)
(ONE-WAY-UNIFY1 TERM1 TERM2))))
(ONE-WAY-UNIFY1
(LAMBDA (TERM1 TERM2)
(COND
((NLISTP TERM2)
(COND
((SETQ TEMP-TEMP (FASSOC TERM2 UNIFY-SUBST))
(EQUAL TERM1 (CDR TEMP-TEMP)))
(T (SETQ UNIFY-SUBST (CONS (CONS TERM2 TERM1)
UNIFY-SUBST))
T)))
((ATOM TERM1)
NIL)
((EQ (CAR TERM1)
(CAR TERM2))
(ONE-WAY-UNIFY1-LST (CDR TERM1)
(CDR TERM2)))
(T NIL))))
(ONE-WAY-UNIFY1-LST
(LAMBDA (LST1 LST2)
(COND
((NULL LST1)
T)
((ONE-WAY-UNIFY1 (CAR LST1)
(CAR LST2))
(ONE-WAY-UNIFY1-LST (CDR LST1)
(CDR LST2)))
(T NIL))))
(PTIME
(LAMBDA NIL
(PROG (GCTM)
(SETQ GCTM (CLOCK 3))
(RETURN (CONS (IPLUS (CLOCK 2)
GCTM)
GCTM)))))
(REWRITE
(LAMBDA (TERM)
(COND
((NLISTP TERM)
TERM)
(T (REWRITE-WITH-LEMMAS (CONS (CAR TERM)
(REWRITE-ARGS (CDR TERM)))
(GETPROP (CAR TERM)
(QUOTE LEMMAS)))))))
(REWRITE-ARGS
(LAMBDA (LST)
(COND
((NULL LST)
NIL)
(T (CONS (REWRITE (CAR LST))
(REWRITE-ARGS (CDR LST)))))))
(REWRITE-WITH-LEMMAS
(LAMBDA (TERM LST)
(COND
((NULL LST)
TERM)
((ONE-WAY-UNIFY TERM (CADR (CAR LST)))
(REWRITE (APPLY-SUBST UNIFY-SUBST (CADDR (CAR LST)))))
(T (REWRITE-WITH-LEMMAS TERM (CDR LST))))))
(SETUP
(LAMBDA NIL
(ADD-LEMMA-LST
(QUOTE
((EQUAL (COMPILE FORM)
(REVERSE (CODEGEN (OPTIMIZE FORM)
(NIL))))
(EQUAL (EQP X Y)
(EQUAL (FIX X)
(FIX Y)))
(EQUAL (GREATERP X Y)
(LESSP Y X))
(EQUAL (LESSEQP X Y)
(NOT (LESSP Y X)))
(EQUAL (GREATEREQP X Y)
(NOT (LESSP X Y)))
(EQUAL (BOOLEAN X)
(OR (EQUAL X (T))
(EQUAL X (F))))
(EQUAL (IFF X Y)
(AND (IMPLIES X Y)
(IMPLIES Y X)))
(EQUAL (EVEN1 X)
(IF (ZEROP X)
(T)
(ODD (SUB1 X))))
(EQUAL (COUNTPS- L PRED)
(COUNTPS-LOOP L PRED (ZERO)))
(EQUAL (FACT- I)
(FACT-LOOP I 1))
(EQUAL (REVERSE- X)
(REVERSE-LOOP X (NIL)))
(EQUAL (DIVIDES X Y)
(ZEROP (REMAINDER Y X)))
(EQUAL (ASSUME-TRUE VAR ALIST)
(CONS (CONS VAR (T))
ALIST))
(EQUAL (ASSUME-FALSE VAR ALIST)
(CONS (CONS VAR (F))
ALIST))
(EQUAL (TAUTOLOGY-CHECKER X)
(TAUTOLOGYP (NORMALIZE X)
(NIL)))
(EQUAL (FALSIFY X)
(FALSIFY1 (NORMALIZE X)
(NIL)))
(EQUAL (PRIME X)
(AND (NOT (ZEROP X))
(NOT (EQUAL X (ADD1 (ZERO))))
(PRIME1 X (SUB1 X))))
(EQUAL (AND P Q)
(IF P (IF Q (T)
(F))
(F)))
(EQUAL (OR P Q)
(IF P (T)
(IF Q (T)
(F))
(F)))
(EQUAL (NOT P)
(IF P (F)
(T)))
(EQUAL (IMPLIES P Q)
(IF P (IF Q (T)
(F))
(T)))
(EQUAL (FIX X)
(IF (NUMBERP X)
X
(ZERO)))
(EQUAL (IF (IF A B C)
D E)
(IF A (IF B D E)
(IF C D E)))
(EQUAL (ZEROP X)
(OR (EQUAL X (ZERO))
(NOT (NUMBERP X))))
(EQUAL (PLUS (PLUS X Y)
Z)
(PLUS X (PLUS Y Z)))
(EQUAL (EQUAL (PLUS A B)
(ZERO))
(AND (ZEROP A)
(ZEROP B)))
(EQUAL (DIFFERENCE X X)
(ZERO))
(EQUAL (EQUAL (PLUS A B)
(PLUS A C))
(EQUAL (FIX B)
(FIX C)))
(EQUAL (EQUAL (ZERO)
(DIFFERENCE X Y))
(NOT (LESSP Y X)))
(EQUAL (EQUAL X (DIFFERENCE X Y))
(AND (NUMBERP X)
(OR (EQUAL X (ZERO))
(ZEROP Y))))
(EQUAL (MEANING (PLUS-TREE (APPEND X Y))
A)
(PLUS (MEANING (PLUS-TREE X)
A)
(MEANING (PLUS-TREE Y)
A)))
(EQUAL (MEANING (PLUS-TREE (PLUS-FRINGE X))
A)
(FIX (MEANING X A)))
(EQUAL (APPEND (APPEND X Y)
Z)
(APPEND X (APPEND Y Z)))
(EQUAL (REVERSE (APPEND A B))
(APPEND (REVERSE B)
(REVERSE A)))
(EQUAL (TIMES X (PLUS Y Z))
(PLUS (TIMES X Y)
(TIMES X Z)))
(EQUAL (TIMES (TIMES X Y)
Z)
(TIMES X (TIMES Y Z)))
(EQUAL (EQUAL (TIMES X Y)
(ZERO))
(OR (ZEROP X)
(ZEROP Y)))
(EQUAL (EXEC (APPEND X Y)
PDS ENVRN)
(EXEC Y (EXEC X PDS ENVRN)
ENVRN))
(EQUAL (MC-FLATTEN X Y)
(APPEND (FLATTEN X)
Y))
(EQUAL (MEMBER X (APPEND A B))
(OR (MEMBER X A)
(MEMBER X B)))
(EQUAL (MEMBER X (REVERSE Y))
(MEMBER X Y))
(EQUAL (LENGTH (REVERSE X))
(LENGTH X))
(EQUAL (MEMBER A (INTERSECT B C))
(AND (MEMBER A B)
(MEMBER A C)))
(EQUAL (NTH (ZERO)
I)
(ZERO))
(EQUAL (EXP I (PLUS J K))
(TIMES (EXP I J)
(EXP I K)))
(EQUAL (EXP I (TIMES J K))
(EXP (EXP I J)
K))
(EQUAL (REVERSE-LOOP X Y)
(APPEND (REVERSE X)
Y))
(EQUAL (REVERSE-LOOP X (NIL))
(REVERSE X))
(EQUAL (COUNT-LIST Z (SORT-LP X Y))
(PLUS (COUNT-LIST Z X)
(COUNT-LIST Z Y)))
(EQUAL (EQUAL (APPEND A B)
(APPEND A C))
(EQUAL B C))
(EQUAL (PLUS (REMAINDER X Y)
(TIMES Y (QUOTIENT X Y)))
(FIX X))
(EQUAL (POWER-EVAL (BIG-PLUS1 L I BASE)
BASE)
(PLUS (POWER-EVAL L BASE)
I))
(EQUAL (POWER-EVAL (BIG-PLUS X Y I BASE)
BASE)
(PLUS I (PLUS (POWER-EVAL X BASE)
(POWER-EVAL Y BASE))))
(EQUAL (REMAINDER Y 1)
(ZERO))
(EQUAL (LESSP (REMAINDER X Y)
Y)
(NOT (ZEROP Y)))
(EQUAL (REMAINDER X X)
(ZERO))
(EQUAL (LESSP (QUOTIENT I J)
I)
(AND (NOT (ZEROP I))
(OR (ZEROP J)
(NOT (EQUAL J 1)))))
(EQUAL (LESSP (REMAINDER X Y)
X)
(AND (NOT (ZEROP Y))
(NOT (ZEROP X))
(NOT (LESSP X Y))))
(EQUAL (POWER-EVAL (POWER-REP I BASE)
BASE)
(FIX I))
(EQUAL (POWER-EVAL (BIG-PLUS (POWER-REP I BASE)
(POWER-REP J BASE)
(ZERO)
BASE)
BASE)
(PLUS I J))
(EQUAL (GCD X Y)
(GCD Y X))
(EQUAL (NTH (APPEND A B)
I)
(APPEND (NTH A I)
(NTH B (DIFFERENCE I (LENGTH A)))))
(EQUAL (DIFFERENCE (PLUS X Y)
X)
(FIX Y))
(EQUAL (DIFFERENCE (PLUS Y X)
X)
(FIX Y))
(EQUAL (DIFFERENCE (PLUS X Y)
(PLUS X Z))
(DIFFERENCE Y Z))
(EQUAL (TIMES X (DIFFERENCE C W))
(DIFFERENCE (TIMES C X)
(TIMES W X)))
(EQUAL (REMAINDER (TIMES X Z)
Z)
(ZERO))
(EQUAL (DIFFERENCE (PLUS B (PLUS A C))
A)
(PLUS B C))
(EQUAL (DIFFERENCE (ADD1 (PLUS Y Z))
Z)
(ADD1 Y))
(EQUAL (LESSP (PLUS X Y)
(PLUS X Z))
(LESSP Y Z))
(EQUAL (LESSP (TIMES X Z)
(TIMES Y Z))
(AND (NOT (ZEROP Z))
(LESSP X Y)))
(EQUAL (LESSP Y (PLUS X Y))
(NOT (ZEROP X)))
(EQUAL (GCD (TIMES X Z)
(TIMES Y Z))
(TIMES Z (GCD X Y)))
(EQUAL (VALUE (NORMALIZE X)
A)
(VALUE X A))
(EQUAL (EQUAL (FLATTEN X)
(CONS Y (NIL)))
(AND (NLISTP X)
(EQUAL X Y)))
(EQUAL (LISTP (GOPHER X))
(LISTP X))
(EQUAL (SAMEFRINGE X Y)
(EQUAL (FLATTEN X)
(FLATTEN Y)))
(EQUAL (EQUAL (GREATEST-FACTOR X Y)
(ZERO))
(AND (OR (ZEROP Y)
(EQUAL Y 1))
(EQUAL X (ZERO))))
(EQUAL (EQUAL (GREATEST-FACTOR X Y)
1)
(EQUAL X 1))
(EQUAL (NUMBERP (GREATEST-FACTOR X Y))
(NOT (AND (OR (ZEROP Y)
(EQUAL Y 1))
(NOT (NUMBERP X)))))
(EQUAL (TIMES-LIST (APPEND X Y))
(TIMES (TIMES-LIST X)
(TIMES-LIST Y)))
(EQUAL (PRIME-LIST (APPEND X Y))
(AND (PRIME-LIST X)
(PRIME-LIST Y)))
(EQUAL (EQUAL Z (TIMES W Z))
(AND (NUMBERP Z)
(OR (EQUAL Z (ZERO))
(EQUAL W 1))))
(EQUAL (GREATEREQPR X Y)
(NOT (LESSP X Y)))
(EQUAL (EQUAL X (TIMES X Y))
(OR (EQUAL X (ZERO))
(AND (NUMBERP X)
(EQUAL Y 1))))
(EQUAL (REMAINDER (TIMES Y X)
Y)
(ZERO))
(EQUAL (EQUAL (TIMES A B)
1)
(AND (NOT (EQUAL A (ZERO)))
(NOT (EQUAL B (ZERO)))
(NUMBERP A)
(NUMBERP B)
(EQUAL (SUB1 A)
(ZERO))
(EQUAL (SUB1 B)
(ZERO))))
(EQUAL (LESSP (LENGTH (DELETE X L))
(LENGTH L))
(MEMBER X L))
(EQUAL (SORT2 (DELETE X L))
(DELETE X (SORT2 L)))
(EQUAL (DSORT X)
(SORT2 X))
(EQUAL
(LENGTH (CONS X1
(CONS X2
(CONS X3
(CONS X4 (CONS X5
(CONS X6 X7)))))))
(PLUS 6 (LENGTH X7)))
(EQUAL (DIFFERENCE (ADD1 (ADD1 X))
2)
(FIX X))
(EQUAL (QUOTIENT (PLUS X (PLUS X Y))
2)
(PLUS X (QUOTIENT Y 2)))
(EQUAL (SIGMA (ZERO)
I)
(QUOTIENT (TIMES I (ADD1 I))
2))
(EQUAL (PLUS X (ADD1 Y))
(IF (NUMBERP Y)
(ADD1 (PLUS X Y))
(ADD1 X)))
(EQUAL (EQUAL (DIFFERENCE X Y)
(DIFFERENCE Z Y))
(IF (LESSP X Y)
(NOT (LESSP Y Z))
(IF (LESSP Z Y)
(NOT (LESSP Y X))
(EQUAL (FIX X)
(FIX Z)))))
(EQUAL (MEANING (PLUS-TREE (DELETE X Y))
A)
(IF (MEMBER X Y)
(DIFFERENCE (MEANING (PLUS-TREE Y)
A)
(MEANING X A))
(MEANING (PLUS-TREE Y)
A)))
(EQUAL (TIMES X (ADD1 Y))
(IF (NUMBERP Y)
(PLUS X (TIMES X Y))
(FIX X)))
(EQUAL (NTH (NIL)
I)
(IF (ZEROP I)
(NIL)
(ZERO)))
(EQUAL (LAST (APPEND A B))
(IF (LISTP B)
(LAST B)
(IF (LISTP A)
(CONS (CAR (LAST A))
B)
B)))
(EQUAL (EQUAL (LESSP X Y)
Z)
(IF (LESSP X Y)
(EQUAL T Z)
(EQUAL F Z)))
(EQUAL (ASSIGNMENT X (APPEND A B))
(IF (ASSIGNEDP X A)
(ASSIGNMENT X A)
(ASSIGNMENT X B)))
(EQUAL (CAR (GOPHER X))
(IF (LISTP X)
(CAR (FLATTEN X))
(ZERO)))
(EQUAL (FLATTEN (CDR (GOPHER X)))
(IF (LISTP X)
(CDR (FLATTEN X))
(CONS (ZERO)
(NIL))))
(EQUAL (QUOTIENT (TIMES Y X)
Y)
(IF (ZEROP Y)
(ZERO)
(FIX X)))
(EQUAL (GET J (SET I VAL MEM))
(IF (EQP J I)
VAL
(GET J MEM))))))))
(TAUTOLOGYP
(LAMBDA (X TRUE-LST FALSE-LST)
(COND
((TRUEP X TRUE-LST)
T)
((FALSEP X FALSE-LST)
NIL)
((NLISTP X)
NIL)
((EQ (CAR X)
(QUOTE IF))
(COND
((TRUEP (CADR X)
TRUE-LST)
(TAUTOLOGYP (CADDR X)
TRUE-LST FALSE-LST))
((FALSEP (CADR X)
FALSE-LST)
(TAUTOLOGYP (CADDDR X)
TRUE-LST FALSE-LST))
(T (AND (TAUTOLOGYP (CADDR X)
(CONS (CADR X)
TRUE-LST)
FALSE-LST)
(TAUTOLOGYP (CADDDR X)
TRUE-LST
(CONS (CADR X)
FALSE-LST))))))
(T NIL))))
(TAUTP
(LAMBDA (X)
(TAUTOLOGYP (REWRITE X)
NIL NIL)))
(TEST
(LAMBDA NIL
(PROG (TM1 TM2 ANS TERM)
(SETQ TM1 (PTIME))
(SETQ TERM
(APPLY-SUBST
(QUOTE ((X F (PLUS (PLUS A B)
(PLUS C (ZERO))))
(Y F (TIMES (TIMES A B)
(PLUS C D)))
(Z F (REVERSE (APPEND (APPEND A B)
(NIL))))
(U EQUAL (PLUS A B)
(DIFFERENCE X Y))
(W LESSP (REMAINDER A B)
(MEMBER A (LENGTH B)))))
(QUOTE (IMPLIES (AND (IMPLIES X Y)
(AND (IMPLIES Y Z)
(AND (IMPLIES Z U)
(IMPLIES U W))))
(IMPLIES X W)))))
(SETQ ANS (TAUTP TERM))
(SETQ TM2 (PTIME))
(RETURN (LIST ANS (DIFFERENCE (CAR TM2)
(CAR TM1))
(DIFFERENCE (CDR TM2)
(CDR TM1)))))))
(TRANS-OF-IMPLIES
(LAMBDA (N)
(LIST (QUOTE IMPLIES)
(TRANS-OF-IMPLIES1 N)
(LIST (QUOTE IMPLIES)
0 N))))
(TRANS-OF-IMPLIES1
(LAMBDA (N)
(COND
((EQUAL N 1)
(LIST (QUOTE IMPLIES)
0 1))
(T (LIST (QUOTE AND)
(LIST (QUOTE IMPLIES)
(SUB1 N)
N)
(TRANS-OF-IMPLIES1 (SUB1 N)))))))
(TRUEP
(LAMBDA (X LST)
(OR (EQUAL X (QUOTE (T)))
(MEMBER X LST))))
)
(PUTPROPS MEMBER BLKLIBRARYDEF (LAMBDA
(.BLKVAR.X .BLKVAR.Y)
(DECLARE (LOCALVARS . T))
(PROG NIL LP (RETURN (COND ((NLISTP .BLKVAR.Y)
NIL)
((EQUAL .BLKVAR.X (CAR .BLKVAR.Y)
)
.BLKVAR.Y)
(T (SETQ .BLKVAR.Y (CDR
.BLKVAR.Y))
(GO LP)))))))
[DECLARE: DONTEVAL@LOAD DOEVAL@COMPILE DONTCOPY
(BLOCK: REWRITEBLOCK ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST
APPLY-SUBST-LST FALSEP ONE-WAY-UNIFY ONE-WAY-UNIFY1
ONE-WAY-UNIFY1-LST PTIME REWRITE REWRITE-ARGS
REWRITE-WITH-LEMMAS SETUP TAUTOLOGYP TAUTP TEST
TRANS-OF-IMPLIES TRANS-OF-IMPLIES1 TRUEP (ENTRIES TEST SETUP)
(BLKLIBRARY EQUAL MEMBER GETPROP)
(GLOBALVARS TEMP-TEMP UNIFY-SUBST))
]
(DECLARE: DONTCOPY
(FILEMAP (NIL (1018 14165 (ADD-LEMMA 1030 . 1573) (ADD-LEMMA-LST 1577 .
1708) (APPLY-SUBST 1712 . 1945) (APPLY-SUBST-LST 1949 . 2119) (FALSEP
2123 . 2200) (ONE-WAY-UNIFY 2204 . 2315) (ONE-WAY-UNIFY1 2319 . 2717) (
ONE-WAY-UNIFY1-LST 2721 . 2928) (PTIME 2932 . 3077) (REWRITE 3081 . 3295
) (REWRITE-ARGS 3299 . 3441) (REWRITE-WITH-LEMMAS 3445 . 3679) (SETUP
3683 . 12295) (TAUTOLOGYP 12299 . 12890) (TAUTP 12894 . 12958) (TEST
12962 . 13720) (TRANS-OF-IMPLIES 13724 . 13846) (TRANS-OF-IMPLIES1 13850
. 14082) (TRUEP 14086 . 14162)))))
STOP
The Maclisp Code
(DECLARE (SPECIAL UNIFY-SUBST TEMP-TEMP))
(DEFUN PTIME NIL (LIST (RUNTIME) (STATUS GCTIME)))
(DEFUN ADD-LEMMA (TERM)
(COND ((AND (NOT (ATOM TERM))
(EQ (CAR TERM)
(QUOTE EQUAL))
(NOT (ATOM (CADR TERM))))
(PUTPROP (CAR (CADR TERM))
(CONS TERM (GET (CAR (CADR TERM))
(QUOTE LEMMAS)))
(QUOTE LEMMAS)))
(T (ERROR (QUOTE ADD-LEMMA-DID-NOT-LIKE-TERM)
TERM))))
(DEFUN ADD-LEMMA-LST (LST)
(COND ((NULL LST)
T)
(T (ADD-LEMMA (CAR LST))
(ADD-LEMMA-LST (CDR LST)))))
(DEFUN APPLY-SUBST (ALIST TERM)
(COND ((ATOM TERM)
(COND ((SETQ TEMP-TEMP (ASSQ TERM ALIST))
(CDR TEMP-TEMP))
(T TERM)))
(T (CONS (CAR TERM)
(APPLY-SUBST-LST ALIST (CDR TERM))))))
(DEFUN APPLY-SUBST-LST (ALIST LST)
(COND ((NULL LST)
NIL)
(T (CONS (APPLY-SUBST ALIST (CAR LST))
(APPLY-SUBST-LST ALIST (CDR LST))))))
(DEFUN FALSEP (X LST)
(OR (EQUAL X (QUOTE (F)))
(MEMBER X LST)))
(DEFUN ONE-WAY-UNIFY (TERM1 TERM2)
(PROGN (SETQ UNIFY-SUBST NIL)
(ONE-WAY-UNIFY1 TERM1 TERM2)))
(DEFUN ONE-WAY-UNIFY1 (TERM1 TERM2)
(COND ((ATOM TERM2)
(COND ((SETQ TEMP-TEMP (ASSQ TERM2 UNIFY-SUBST))
(EQUAL TERM1 (CDR TEMP-TEMP)))
(T (SETQ UNIFY-SUBST (CONS (CONS TERM2 TERM1)
UNIFY-SUBST))
T)))
((ATOM TERM1)
NIL)
((EQ (CAR TERM1)
(CAR TERM2))
(ONE-WAY-UNIFY1-LST (CDR TERM1)
(CDR TERM2)))
(T NIL)))
(DEFUN ONE-WAY-UNIFY1-LST (LST1 LST2)
(COND ((NULL LST1)
T)
((ONE-WAY-UNIFY1 (CAR LST1)
(CAR LST2))
(ONE-WAY-UNIFY1-LST (CDR LST1)
(CDR LST2)))
(T NIL)))
(DEFUN REWRITE (TERM)
(COND ((ATOM TERM)
TERM)
(T (REWRITE-WITH-LEMMAS (CONS (CAR TERM)
(REWRITE-ARGS (CDR TERM)))
(GET (CAR TERM)
(QUOTE LEMMAS))))))
(DEFUN REWRITE-ARGS (LST)
(COND ((NULL LST)
NIL)
(T (CONS (REWRITE (CAR LST))
(REWRITE-ARGS (CDR LST))))))
(DEFUN REWRITE-WITH-LEMMAS (TERM LST)
(COND ((NULL LST)
TERM)
((ONE-WAY-UNIFY TERM (CADR (CAR LST)))
(REWRITE (APPLY-SUBST UNIFY-SUBST (CADDR (CAR LST)))))
(T (REWRITE-WITH-LEMMAS TERM (CDR LST)))))
(DEFUN
SETUP NIL
(ADD-LEMMA-LST
(QUOTE ((EQUAL (COMPILE FORM)
(REVERSE (CODEGEN (OPTIMIZE FORM)
(NIL))))
(EQUAL (EQP X Y)
(EQUAL (FIX X)
(FIX Y)))
(EQUAL (GREATERP X Y)
(LESSP Y X))
(EQUAL (LESSEQP X Y)
(NOT (LESSP Y X)))
(EQUAL (GREATEREQP X Y)
(NOT (LESSP X Y)))
(EQUAL (BOOLEAN X)
(OR (EQUAL X (T))
(EQUAL X (F))))
(EQUAL (IFF X Y)
(AND (IMPLIES X Y)
(IMPLIES Y X)))
(EQUAL (EVEN1 X)
(IF (ZEROP X)
(T)
(ODD (SUB1 X))))
(EQUAL (COUNTPS- L PRED)
(COUNTPS-LOOP L PRED (ZERO)))
(EQUAL (FACT- I)
(FACT-LOOP I 1))
(EQUAL (REVERSE- X)
(REVERSE-LOOP X (NIL)))
(EQUAL (DIVIDES X Y)
(ZEROP (REMAINDER Y X)))
(EQUAL (ASSUME-TRUE VAR ALIST)
(CONS (CONS VAR (T))
ALIST))
(EQUAL (ASSUME-FALSE VAR ALIST)
(CONS (CONS VAR (F))
ALIST))
(EQUAL (TAUTOLOGY-CHECKER X)
(TAUTOLOGYP (NORMALIZE X)
(NIL)))
(EQUAL (FALSIFY X)
(FALSIFY1 (NORMALIZE X)
(NIL)))
(EQUAL (PRIME X)
(AND (NOT (ZEROP X))
(NOT (EQUAL X (ADD1 (ZERO))))
(PRIME1 X (SUB1 X))))
(EQUAL (AND P Q)
(IF P (IF Q (T)
(F))
(F)))
(EQUAL (OR P Q)
(IF P (T)
(IF Q (T)
(F))
(F)))
(EQUAL (NOT P)
(IF P (F)
(T)))
(EQUAL (IMPLIES P Q)
(IF P (IF Q (T)
(F))
(T)))
(EQUAL (FIX X)
(IF (NUMBERP X)
X
(ZERO)))
(EQUAL (IF (IF A B C)
D E)
(IF A (IF B D E)
(IF C D E)))
(EQUAL (ZEROP X)
(OR (EQUAL X (ZERO))
(NOT (NUMBERP X))))
(EQUAL (PLUS (PLUS X Y)
Z)
(PLUS X (PLUS Y Z)))
(EQUAL (EQUAL (PLUS A B)
(ZERO))
(AND (ZEROP A)
(ZEROP B)))
(EQUAL (DIFFERENCE X X)
(ZERO))
(EQUAL (EQUAL (PLUS A B)
(PLUS A C))
(EQUAL (FIX B)
(FIX C)))
(EQUAL (EQUAL (ZERO)
(DIFFERENCE X Y))
(NOT (LESSP Y X)))
(EQUAL (EQUAL X (DIFFERENCE X Y))
(AND (NUMBERP X)
(OR (EQUAL X (ZERO))
(ZEROP Y))))
(EQUAL (MEANING (PLUS-TREE (APPEND X Y))
A)
(PLUS (MEANING (PLUS-TREE X)
A)
(MEANING (PLUS-TREE Y)
A)))
(EQUAL (MEANING (PLUS-TREE (PLUS-FRINGE X))
A)
(FIX (MEANING X A)))
(EQUAL (APPEND (APPEND X Y)
Z)
(APPEND X (APPEND Y Z)))
(EQUAL (REVERSE (APPEND A B))
(APPEND (REVERSE B)
(REVERSE A)))
(EQUAL (TIMES X (PLUS Y Z))
(PLUS (TIMES X Y)
(TIMES X Z)))
(EQUAL (TIMES (TIMES X Y)
Z)
(TIMES X (TIMES Y Z)))
(EQUAL (EQUAL (TIMES X Y)
(ZERO))
(OR (ZEROP X)
(ZEROP Y)))
(EQUAL (EXEC (APPEND X Y)
PDS ENVRN)
(EXEC Y (EXEC X PDS ENVRN)
ENVRN))
(EQUAL (MC-FLATTEN X Y)
(APPEND (FLATTEN X)
Y))
(EQUAL (MEMBER X (APPEND A B))
(OR (MEMBER X A)
(MEMBER X B)))
(EQUAL (MEMBER X (REVERSE Y))
(MEMBER X Y))
(EQUAL (LENGTH (REVERSE X))
(LENGTH X))
(EQUAL (MEMBER A (INTERSECT B C))
(AND (MEMBER A B)
(MEMBER A C)))
(EQUAL (NTH (ZERO)
I)
(ZERO))
(EQUAL (EXP I (PLUS J K))
(TIMES (EXP I J)
(EXP I K)))
(EQUAL (EXP I (TIMES J K))
(EXP (EXP I J)
K))
(EQUAL (REVERSE-LOOP X Y)
(APPEND (REVERSE X)
Y))
(EQUAL (REVERSE-LOOP X (NIL))
(REVERSE X))
(EQUAL (COUNT-LIST Z (SORT-LP X Y))
(PLUS (COUNT-LIST Z X)
(COUNT-LIST Z Y)))
(EQUAL (EQUAL (APPEND A B)
(APPEND A C))
(EQUAL B C))
(EQUAL (PLUS (REMAINDER X Y)
(TIMES Y (QUOTIENT X Y)))
(FIX X))
(EQUAL (POWER-EVAL (BIG-PLUS1 L I BASE)
BASE)
(PLUS (POWER-EVAL L BASE)
I))
(EQUAL (POWER-EVAL (BIG-PLUS X Y I BASE)
BASE)
(PLUS I (PLUS (POWER-EVAL X BASE)
(POWER-EVAL Y BASE))))
(EQUAL (REMAINDER Y 1)
(ZERO))
(EQUAL (LESSP (REMAINDER X Y)
Y)
(NOT (ZEROP Y)))
(EQUAL (REMAINDER X X)
(ZERO))
(EQUAL (LESSP (QUOTIENT I J)
I)
(AND (NOT (ZEROP I))
(OR (ZEROP J)
(NOT (EQUAL J 1)))))
(EQUAL (LESSP (REMAINDER X Y)
X)
(AND (NOT (ZEROP Y))
(NOT (ZEROP X))
(NOT (LESSP X Y))))
(EQUAL (POWER-EVAL (POWER-REP I BASE)
BASE)
(FIX I))
(EQUAL (POWER-EVAL (BIG-PLUS (POWER-REP I BASE)
(POWER-REP J BASE)
(ZERO)
BASE)
BASE)
(PLUS I J))
(EQUAL (GCD X Y)
(GCD Y X))
(EQUAL (NTH (APPEND A B)
I)
(APPEND (NTH A I)
(NTH B (DIFFERENCE I (LENGTH A)))))
(EQUAL (DIFFERENCE (PLUS X Y)
X)
(FIX Y))
(EQUAL (DIFFERENCE (PLUS Y X)
X)
(FIX Y))
(EQUAL (DIFFERENCE (PLUS X Y)
(PLUS X Z))
(DIFFERENCE Y Z))
(EQUAL (TIMES X (DIFFERENCE C W))
(DIFFERENCE (TIMES C X)
(TIMES W X)))
(EQUAL (REMAINDER (TIMES X Z)
Z)
(ZERO))
(EQUAL (DIFFERENCE (PLUS B (PLUS A C))
A)
(PLUS B C))
(EQUAL (DIFFERENCE (ADD1 (PLUS Y Z))
Z)
(ADD1 Y))
(EQUAL (LESSP (PLUS X Y)
(PLUS X Z))
(LESSP Y Z))
(EQUAL (LESSP (TIMES X Z)
(TIMES Y Z))
(AND (NOT (ZEROP Z))
(LESSP X Y)))
(EQUAL (LESSP Y (PLUS X Y))
(NOT (ZEROP X)))
(EQUAL (GCD (TIMES X Z)
(TIMES Y Z))
(TIMES Z (GCD X Y)))
(EQUAL (VALUE (NORMALIZE X)
A)
(VALUE X A))
(EQUAL (EQUAL (FLATTEN X)
(CONS Y (NIL)))
(AND (NLISTP X)
(EQUAL X Y)))
(EQUAL (LISTP (GOPHER X))
(LISTP X))
(EQUAL (SAMEFRINGE X Y)
(EQUAL (FLATTEN X)
(FLATTEN Y)))
(EQUAL (EQUAL (GREATEST-FACTOR X Y)
(ZERO))
(AND (OR (ZEROP Y)
(EQUAL Y 1))
(EQUAL X (ZERO))))
(EQUAL (EQUAL (GREATEST-FACTOR X Y)
1)
(EQUAL X 1))
(EQUAL (NUMBERP (GREATEST-FACTOR X Y))
(NOT (AND (OR (ZEROP Y)
(EQUAL Y 1))
(NOT (NUMBERP X)))))
(EQUAL (TIMES-LIST (APPEND X Y))
(TIMES (TIMES-LIST X)
(TIMES-LIST Y)))
(EQUAL (PRIME-LIST (APPEND X Y))
(AND (PRIME-LIST X)
(PRIME-LIST Y)))
(EQUAL (EQUAL Z (TIMES W Z))
(AND (NUMBERP Z)
(OR (EQUAL Z (ZERO))
(EQUAL W 1))))
(EQUAL (GREATEREQPR X Y)
(NOT (LESSP X Y)))
(EQUAL (EQUAL X (TIMES X Y))
(OR (EQUAL X (ZERO))
(AND (NUMBERP X)
(EQUAL Y 1))))
(EQUAL (REMAINDER (TIMES Y X)
Y)
(ZERO))
(EQUAL (EQUAL (TIMES A B)
1)
(AND (NOT (EQUAL A (ZERO)))
(NOT (EQUAL B (ZERO)))
(NUMBERP A)
(NUMBERP B)
(EQUAL (SUB1 A)
(ZERO))
(EQUAL (SUB1 B)
(ZERO))))
(EQUAL (LESSP (LENGTH (DELETE X L))
(LENGTH L))
(MEMBER X L))
(EQUAL (SORT2 (DELETE X L))
(DELETE X (SORT2 L)))
(EQUAL (DSORT X)
(SORT2 X))
(EQUAL (LENGTH (CONS X1
(CONS X2
(CONS X3 (CONS X4
(CONS X5
(CONS X6 X7)))))))
(PLUS 6 (LENGTH X7)))
(EQUAL (DIFFERENCE (ADD1 (ADD1 X))
2)
(FIX X))
(EQUAL (QUOTIENT (PLUS X (PLUS X Y))
2)
(PLUS X (QUOTIENT Y 2)))
(EQUAL (SIGMA (ZERO)
I)
(QUOTIENT (TIMES I (ADD1 I))
2))
(EQUAL (PLUS X (ADD1 Y))
(IF (NUMBERP Y)
(ADD1 (PLUS X Y))
(ADD1 X)))
(EQUAL (EQUAL (DIFFERENCE X Y)
(DIFFERENCE Z Y))
(IF (LESSP X Y)
(NOT (LESSP Y Z))
(IF (LESSP Z Y)
(NOT (LESSP Y X))
(EQUAL (FIX X)
(FIX Z)))))
(EQUAL (MEANING (PLUS-TREE (DELETE X Y))
A)
(IF (MEMBER X Y)
(DIFFERENCE (MEANING (PLUS-TREE Y)
A)
(MEANING X A))
(MEANING (PLUS-TREE Y)
A)))
(EQUAL (TIMES X (ADD1 Y))
(IF (NUMBERP Y)
(PLUS X (TIMES X Y))
(FIX X)))
(EQUAL (NTH (NIL)
I)
(IF (ZEROP I)
(NIL)
(ZERO)))
(EQUAL (LAST (APPEND A B))
(IF (LISTP B)
(LAST B)
(IF (LISTP A)
(CONS (CAR (LAST A))
B)
B)))
(EQUAL (EQUAL (LESSP X Y)
Z)
(IF (LESSP X Y)
(EQUAL T Z)
(EQUAL F Z)))
(EQUAL (ASSIGNMENT X (APPEND A B))
(IF (ASSIGNEDP X A)
(ASSIGNMENT X A)
(ASSIGNMENT X B)))
(EQUAL (CAR (GOPHER X))
(IF (LISTP X)
(CAR (FLATTEN X))
(ZERO)))
(EQUAL (FLATTEN (CDR (GOPHER X)))
(IF (LISTP X)
(CDR (FLATTEN X))
(CONS (ZERO)
(NIL))))
(EQUAL (QUOTIENT (TIMES Y X)
Y)
(IF (ZEROP Y)
(ZERO)
(FIX X)))
(EQUAL (GET J (SET I VAL MEM))
(IF (EQP J I)
VAL
(GET J MEM)))))))
(DEFUN TAUTOLOGYP (X TRUE-LST FALSE-LST)
(COND ((TRUEP X TRUE-LST)
T)
((FALSEP X FALSE-LST)
NIL)
((ATOM X)
NIL)
((EQ (CAR X)
(QUOTE IF))
(COND ((TRUEP (CADR X)
TRUE-LST)
(TAUTOLOGYP (CADDR X)
TRUE-LST FALSE-LST))
((FALSEP (CADR X)
FALSE-LST)
(TAUTOLOGYP (CADDDR X)
TRUE-LST FALSE-LST))
(T (AND (TAUTOLOGYP (CADDR X)
(CONS (CADR X)
TRUE-LST)
FALSE-LST)
(TAUTOLOGYP (CADDDR X)
TRUE-LST
(CONS (CADR X)
FALSE-LST))))))
(T NIL)))
(DEFUN TAUTP (X)
(TAUTOLOGYP (REWRITE X)
NIL NIL))
(DEFUN TEST NIL
(PROG (TM1 TM2 ANS TERM)
(SETQ TM1 (PTIME))
(SETQ TERM
(APPLY-SUBST
(QUOTE ((X F (PLUS (PLUS A B)
(PLUS C (ZERO))))
(Y F (TIMES (TIMES A B)
(PLUS C D)))
(Z F (REVERSE (APPEND (APPEND A B)
(NIL))))
(U EQUAL (PLUS A B)
(DIFFERENCE X Y))
(W LESSP (REMAINDER A B)
(MEMBER A (LENGTH B)))))
(QUOTE (IMPLIES (AND (IMPLIES X Y)
(AND (IMPLIES Y Z)
(AND (IMPLIES Z U)
(IMPLIES U W))))
(IMPLIES X W)))))
(SETQ ANS (TAUTP TERM))
(SETQ TM2 (PTIME))
(RETURN (LIST ANS (DIFFERENCE (CAR TM2)
(CAR TM1))
(DIFFERENCE (CADR TM2)
(CADR TM1))))))
(DEFUN TRANS-OF-IMPLIES (N)
(LIST (QUOTE IMPLIES)
(TRANS-OF-IMPLIES1 N)
(LIST (QUOTE IMPLIES)
0 N)))
(DEFUN TRANS-OF-IMPLIES1 (N)
(COND ((EQUAL N 1)
(LIST (QUOTE IMPLIES)
0 1))
(T (LIST (QUOTE AND)
(LIST (QUOTE IMPLIES)
(SUB1 N)
N)
(TRANS-OF-IMPLIES1 (SUB1 N))))))
(DEFUN TRUEP (X LST)
(OR (EQUAL X (QUOTE (T)))
(MEMBER X LST)))
The ELISP test
[PHOTO: Recording initiated Tue 29-Jun-82 12:23PM]
LINK FROM CL.BOYER, TTY 17
Tops-20 Command Processor 4A(67)-1
End of <CL.BOYER>COMAND.CMD.1
@<ELISP>ELISP
[Keeping]
Elisp, 4 27 82
*(DSKIN "EREWRITE.FLAP")
"EREWRITE.FLAP.2"
Files-Loaded
*(SETUP)
T
*(TEST)
19776 msec CPU (7447 msec GC), 41583 msec clock, 452930 words consed
(T)
*(TEST)
18185 msec CPU (6361 msec GC), 51621 msec clock, 452930 words consed
(T)
*↑C
@POP
[PHOTO: Recording terminated Tue 29-Jun-82 12:26PM]
Interlisp bcompl blocklib swap and noswap
[PHOTO: Recording initiated Mon 5-Jul-82 12:16PM]
LINK FROM CL.BOYER, TTY 17
Tops-20 Command Processor 4B(70)-1
End of <CL.BOYER>COMAND.CMD.1
@LISP.EXE.133
INTERLISP-10 27-NOV-79 ...
collecting lists
716, 10444 free cells
control-A is an interrupt and can't be an edit control-character
Good afternoon, Bob.
2←LOAD(IREWRITE.COM]
compiled on 5-Jul-82 12:11:29
FILE CREATED 5-Jul-82 12:11:22
IREWRITECOMS
<CL.BOYER.LISPS>IREWRITE.COM.3
3←IREWRITECOMS
((FNS * IREWRITEFNS) (PROP BLKLIBRARYDEF MEMBER SASSOC) (BLOCKS (REWRITEBLOCK
ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST APPLY-SUBST-LST FALSEP ONE-WAY-UNIFY
ONE-WAY-UNIFY1 ONE-WAY-UNIFY1-LST PTIME REWRITE REWRITE-ARGS REWRITE-WITH-LEMMAS
SETUP TAUTOLOGYP TAUTP TEST TRANS-OF-IMPLIES TRANS-OF-IMPLIES1 TRUEP (ENTRIES
TEST SETUP) (BLKLIBRARY EQUAL MEMBER GETPROP) (GLOBALVARS TEMP-TEMP UNIFY-SUBST)
)))
4←NOSWAPFLG
NIL
5←(MINFS 100000]
10000
6←(RECLAIM]
collecting lists
7245, 92749 free cells, 0 pages left
92749
7←(GCGAG]
40
8←(MINFS 10000]
100000
9←SETUP]
T
10←(TEST]
(T 15821 4995)
11←(TEST]
(T 17498 6245)
12←(TEST]
(T 16569 5954)
13←(TEST]
(T 16707 5925)
14←(SETQ NOSWAPFLG T]
(NOSWAPFLG reset)
T
15←LOAD(IREWRITE.COM]
compiled on 5-Jul-82 12:11:29
FILE CREATED 5-Jul-82 12:11:22
(REWRITEBLOCK redefined)
(TEST redefined)
(SETUP redefined)
IREWRITECOMS
<CL.BOYER.LISPS>IREWRITE.COM.3
16←TEST]
(T 19546 8561)
17←TEST]
(T 17431 6601)
18←TEST]
(T 17192 6511)
19←TEST]
(T 18785 8161)
20←↑C
@POP
[PHOTO: Recording terminated Mon 5-Jul-82 12:29PM]
Interlisp bcompl no blocklib swap and noswap
[PHOTO: Recording initiated Mon 5-Jul-82 12:29PM]
LINK FROM CL.BOYER, TTY 17
Tops-20 Command Processor 4B(70)-1
End of <CL.BOYER>COMAND.CMD.1
@LISP.EXE.133
INTERLISP-10 27-NOV-79 ...
collecting lists
716, 10444 free cells
control-A is an interrupt and can't be an edit control-character
Hello, Bob.
2←LOAD(IREWRITE]
FILE CREATED 5-Jul-82 12:11:22
IREWRITECOMS
<CL.BOYER.LISPS>IREWRITE..3
3←IREWRITECOMS
((FNS * IREWRITEFNS) (PROP BLKLIBRARYDEF MEMBER SASSOC) (BLOCKS (REWRITEBLOCK
ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST APPLY-SUBST-LST FALSEP ONE-WAY-UNIFY
ONE-WAY-UNIFY1 ONE-WAY-UNIFY1-LST PTIME REWRITE REWRITE-ARGS REWRITE-WITH-LEMMAS
SETUP TAUTOLOGYP TAUTP TEST TRANS-OF-IMPLIES TRANS-OF-IMPLIES1 TRUEP (ENTRIES
TEST SETUP) (BLKLIBRARY EQUAL MEMBER GETPROP) (GLOBALVARS TEMP-TEMP UNIFY-SUBST)
)))
4←(BLOCKCOMPILE 'REWRITEBLOCK IREWRITEFNS '(TEST SETUP]
listing? STore and redefine
output file? No
(REWRITEBLOCK ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST APPLY-SUBST-LST FALSEP
ONE-WAY-UNIFY ONE-WAY-UNIFY1 ONE-WAY-UNIFY1-LST PTIME REWRITE REWRITE-ARGS
REWRITE-WITH-LEMMAS SETUP TAUTOLOGYP TAUTP TEST TRANS-OF-IMPLIES
TRANS-OF-IMPLIES1 TRUEP)
(REWRITEBLOCK (REWRITEBLOCK#0) (TEMP-TEMP UNIFY-SUBST))
collecting lists
6001, 10097 free cells
(TEST NIL NIL)
(TEST redefined)
(SETUP NIL NIL)
(SETUP redefined)
(TEST SETUP)
5←(SETUP]
T
6←(MINFS 100000]
10000
7←(RECLAIM]
collecting lists
9850, 90234 free cells, 0 pages left
90234
8←(MINFS 10000]
100000
9←(GCGAG]
40
10←NOSWAPFLG
NIL
11←(TEST]
(T 31978 6737)
12←(TEST]
(T 47072 6180)
13←(TEST]
LISP Running at 30547 Used 0:10:10.7 in 2:40:39, Load 3.06
(T 71046 6316)
14←(TEST]
LISP Running at 30525 Used 0:11:45.7 in 2:44:33, Load 2.85
(T 71222 7772)
15←(TEST]
(T 70026 6175)
16←(SETQ NOSWAPFLG T]
(NOSWAPFLG reset)
T
17←REDO BLOCKCOMPILE
listing? ST
output file? N
(REWRITEBLOCK ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST APPLY-SUBST-LST FALSEP
ONE-WAY-UNIFY ONE-WAY-UNIFY1 ONE-WAY-UNIFY1-LST PTIME REWRITE REWRITE-ARGS
REWRITE-WITH-LEMMAS SETUP TAUTOLOGYP TAUTP TEST TRANS-OF-IMPLIES
TRANS-OF-IMPLIES1 TRUEP)
(REWRITEBLOCK (REWRITEBLOCK#0) (TEMP-TEMP UNIFY-SUBST))
(REWRITEBLOCK redefined)
(TEST NIL NIL)
(TEST redefined)
(SETUP NIL NIL)
(SETUP redefined)
(TEST SETUP)
18←(TEST]
(T 46501 7685)
19←TEST]
(T 45285 6068)
20←TEST]
(T 46995 7564)
21←TEST]
(T 46522 6180)
22←↑C
@POP
[PHOTO: Recording terminated Mon 5-Jul-82 12:51PM]
Maclisp
[PHOTO: Recording initiated Tue 29-Jun-82 12:26PM]
LINK FROM CL.BOYER, TTY 17
Tops-20 Command Processor 4A(67)-1
End of <CL.BOYER>COMAND.CMD.1
@<ATP.MURRAY>MACLSP
LISP 1983
Alloc? Y
# REGPDL = 4000
# SPECPDL = 2000
# FXPDL = 4000
# FLPDL = 1000
LIST = 40000 100000.
SYMBOL = 6000 $
*
(SETQ BASE (SETQ IBASE 10.))
10.
(FASLOAD MREWRITE)
40307.
(SETUP)
T
(TEST)
(T 20190000. 11905000.)
(TEST)
(T 13728000. 5236000.)
(TEST)
(T 13708000. 5398000.)
↑C
@POP
[PHOTO: Recording terminated Tue 29-Jun-82 12:29PM]
**********************************************************************
UCILISP
[PHOTO: Recording initiated Wed 30-Jun-82 12:16PM]
LINK FROM CL.BOYER, TTY 17
Tops-20 Command Processor 4B(70)-1
End of <CL.BOYER>COMAND.CMD.1
@
@ucilsp
UT/UCI LISP - 8/10/80
*(gcgag t)
NIL
*(gc)
3790 FREE STG, 1129 FULL WORDS AVAILABLE
NIL
*(expfs 100000.)
FREE STG EXHAUSTED
FULL WORD SPACE EXHAUSTED
101112 FREE STG, 1131 FULL WORDS AVAILABLE
*(loa≠≠≠≠Jdskin (rewrit.lap))
(ADD-LEMMA 32) (ADD-LEMMA-LST 10) (APPLY-SUBST 23) (APPLY-SUBST-LST 15)
(FALSEP 10) (ONE-WAY-UNIFY 2)
Binary Program Space exceeded
*(expbps 1000)
FREE STG EXHAUSTED
FULL WORD SPACE EXHAUSTED
101012 FREE STG, 1091 FULL WORDS AVAILABLE
*(dskin (rewrit.lap))
(ADD-LEMMA 32) (ADD-LEMMA-LST 10) (APPLY-SUBST 23) (APPLY-SUBST-LST 15)
(FALSEP 10) (ONE-WAY-UNIFY 2) (ONE-WAY-UNIFY1 38) (ONE-WAY-UNIFY1-LST 15)
(REWRITE 20) (REWRITE-ARGS 11) (REWRITE-WITH-LEMMAS 22) (SETUP 2) (TAUTOLOGYP
66) (TAUTP 4) (TEST 2) (TEST1 8) (TRANS-OF-IMPLIES 13) (TRANS-OF-IMPLIES1 31)
(TRUEP 10)
FILES-LOADED
*(setup)
T
*(test)
FREE STG EXHAUSTED
63969 FREE STG, 943 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
47018 FREE STG, 943 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
40438 FREE STG, 943 FULL WORDS AVAILABLE
50614 msec CPU (3738 msec GC), 67496 msec clock, 226465 conses
(T)
*(test)
FREE STG EXHAUSTED
94012 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
58810 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
47089 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
35091 FREE STG, 942 FULL WORDS AVAILABLE
51676 msec CPU (4605 msec GC), 72196 msec clock, 226467 conses
(T)
*(test)
FREE STG EXHAUSTED
91609 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
57005 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
45700 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
34252 FREE STG, 942 FULL WORDS AVAILABLE
52328 msec CPU (4809 msec GC), 70687 msec clock, 226467 conses
(T)
*(nouuo nil)
T
*(test)
FREE STG EXHAUSTED
89843 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
56841 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
45727 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
34117 FREE STG, 942 FULL WORDS AVAILABLE
14099 msec CPU (4711 msec GC), 20077 msec clock, 226467 conses
(T)
*(test)
FREE STG EXHAUSTED
89806 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
56830 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
45727 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
34117 FREE STG, 942 FULL WORDS AVAILABLE
13827 msec CPU (4712 msec GC), 19857 msec clock, 226467 conses
(T)
*
@pop
[PHOTO: Recording terminated Wed 30-Jun-82 12:24PM]
Interlisp (Dolphin and Dorado)
Date: 8 Jul 1982 18:56 PDT
From: JonL at PARC-MAXC
Reply-To: JonL at PARC-MAXC
To: NOVAK at SUMEX-AIM
cc: CL.BOYER, Masinter at PARC-MAXC, LispCore↑ at PARC-MAXC
Re: The Boyer-Moore-Novak Benchmarkings
Gordon, I'll have to apologize for waiting so long to get you the results
of the timing comparisons between your machine and the various
configurations at PARC. I was "laid-low" last Saturday with either a
summer flu, or a severe allergic reaction (hay fever), and couldn't get
the results summarized until yesterday.
I have six areas that I want to summarize in this note:
Translation Inadequacy due to the FreeVars Trip-Up
"Ineffable" Factors Tending to make timing runs Un-Reproducible
PUP Activity -- Ephemeral as well as Ineffable
What the Faster Clock on buys
What DISPLAYDOWN buys
What you can Expect for Dolphin Speed Increases Soon
Briefly, the "FreeVars Trip-Up" and the DISPLAYDOWN account
for most of the sluggishness of the timings you made, but also there's
one "ineffable" which might be sabotaging you.
Below these sections, I've tried to display my data in good scientific
fashion; you'll note that I give a "First run" time and a "Mode run" time.
What this means is the "First run" must absorb all the "ineffable" costs of
swapping in the necessary code and data parts, and of initially-building
the List-space pages that will be used and re-used on subsequent runs.
Also included are one set of timings from a Dorado, just for comparison.
Generally, my comparisons will be of "speed" rather than "time". Thus
if one trial takes 40 secs, and another takes 50 secs, then the first one
runs 25% faster (the other way of saying it would be that the first one
takes 20% less time). The rationale is this: the first one "computes"
.025 MegaFrumbles per second, while the second one only computes
.020 MegaFrumbles per second; hence the speed of the first one is
(.025-.020)/.020 = 25% faster than the speed of the second one.
Translation Inadequacy due to the FreeVars Trip-Up
Actually, it's just as well that I waited until today to report to you,
since the **major factor** in the timings compared so far is the old
"FreeVars Trip-Up", and anyway Boyer's latest modification is more
appropriate for benchmarking, period. I have quite a few interesting
timings to report (and a few remaining mysteries regarding your
machine), but indeed the major discrepancy between your timings
and mine was that the version of IREWRITE we had at Parc is the one
that Larry had "diddled" as per his earlier note.
On your machine, I saw a 50% speedup due to better treatment of the
free variable TEMP-TEMP. (My runs of your original version of
IREWRITE compared with Larry's "diddled" version).
On several machines here, I compared Larry's "diddled" version with
Boyer's new version, and observed about a 9% speed-up of the latter
over the former. Converting TEMP-TEMP from a local variable to a
GLOBALVAR should cause a slowdown in the 1% range (a GLOBALVAR
usage may take time for a GC-hash-table operation, but a LOCALVAR
usage takes time only for pushing/popping the stack) but Boyer changed
several other bottlenecks and the speed increases therefrom more than
compensated for the loss of the local variable (SASSOC ==> FASSOC,
and the placement of important properties at the beginning of the proplist ?)
In any case, this benchmark exhibits a factor of two improvement by
removing what I'm calling the "FreeVars Trip-Up".
This point can't be overstressed: that Interlisp-D is a deep-bound
implementation, whereas MacLisp and current Interlisp-10 are shallow-
bound (Interlisp-10 was first deep-bound, then later shallow-bound),
and that the questionable practice of using free variables for local
temporaries costs little when they are shallow-bound, but could
cost arbitrarily large when deep-bound. I say, "questionable" since a
program with such temporaries is semantically the same regardless of
whether they are GLOBAL, SPECIAL, or local; furthermore, the
general direction of "structured programming" is to avoid free variables
at all costs, and to bind temporaries as syntactically "low" as possible.
The *default* declaration for variables in Interlisp is SPECVARS, for
consistency with the way the interpreter is written, and thus the default
compilation of a free variable will cause a stack scan (slow) rather than a
reference to the global value cell (fast). So one does have to take *some*
action to override the default case when transporting such a program.
A recent Symbolics advertising flyer makes a "comparison" of an Interlisp
program running on the Dolphin and on the LM-2. It wasn't so much
a comparison between Interlisp-D/Dolphin with ZetaLisp/CADR as a
documentation of someone's failure to add the appropriate GLOBALVARS
delcarations. I heard (admittedly, hearsay) that the ISI guy whose program
was under test made the additional declaration himself, and the Dolphin
performance "improved by 67%". [One also wonders how the "comparison"
would have fared had the LISPMachine garbage collector been operable;
a large percentage of the Dolphin time was spent in GC, which helps keep
the working-set small, and also allows you to continue running *after*
the benchmark has finished running.]
"Ineffable" Factors Tending to make timing runs Un-Reproducible
As Larry's note indicated, there is a hidden problem with swap time in
the Interlisp-D of today -- an "ineffable" amount of it is being charged
to CPU time rather than the reported Swap time. The data below seem
to indicate anywhere from 5% to 20% of reported CPU time is really swap
time, when there is indeed swapping going on.
You're quite right, however, that swapping-time is a small factor in this
benchmark; although there consistently seemed to be more of it on your
machine than mine (about 8%, depending on method of interpretation of
the "ineffable" considerations herein mentioned). That's mystery number 1,
since both your machine and mine have the same amount of real memory,
namely about 1.15 Megabyte. The proper setting of RECLAIMMIN keeps
both our Dolphins from "going over the knee" on this benchmark, although
a large setting for my Dolphin caused the CPU time to go up by 50%
and the Swap time to go up from essentially 0 to almost 600 seconds. A
Dorado, with 2 Megabytes and a faster swapping-disk, didn't "go over the
knee" even with the extreme high setting of RECLAIMMIN.
During the first run of TEST, additional pages are added to LIST space,
and the cost of doing this is difficult to estimate accurately in the current
setup. The STATS I ran on the Dorado showed nearly 20% of the
total first-run time given to this activity, but this is inflated by the
fact that the run had to be terminated abnormally (ran out of DSK space
for keeping statistics); this "ineffable" time would concentrate in the
early part of the run. But a 5%-10% slowdown due to this facter seems
indicated in general (my "educated guess" from mulling over the data).
There is a certain oddity about the reference-count GC scheme in that
a call to RECLAIM may not necessarily recover all reclaimable space.
Without going into the details of this oddity, I merely observed that
between TEST runs, it was necessary to do several iterations of
(R@
→β∪~$AEKM=eJAi!JAiS5JAga∃]hAi!KeKS8AgKiQYKHA⊃←o\AQ↑ABAQsaSG¬XAY←\~∃mC1kJA7%]ISG¬iS]N↓iQCh↓[←gh↓SLA]=hACY0AeKG1CS[C YKfA]KeJA%\AMC
hAeK
YCS[∃I:\~(~∃)Q%fASf↓oQrA$OmJA%]ISG¬iKHA∧@E[←⊃JDAeU\@ZZ↓]C[K1rAiQ∀AiS[%]OfAQQChA¬eJ@~)[←gh↓←MiK8AgKK8ACMi∃dAiQ∀AS]SQSCXAMoC`[%\XAS9SiSC0AgoK1X[k`↓←LA→%'(AgACGJX4∃C]HEGYK¬]]KgLDA←L↓iQJAIKGYC%[CEY∀AgaC
JACe∀ACGG=k]iK⊂AM←d8@A¬kPA∩A[Ugh~∃
←]MKMfXAi!ChA∩↓QCI\≥hAISMG←mKIKHAC1XA←L↓iQKg∀AiQS9OfAS9SiSC1YrXAM↑AiQ∃eJASL@~∃B↓YSii1JAk]
KeiC%]irA¬E←kh↓iQJ@ [←IJλAiS[%]OfA⊃←]JA=\A∃k1r@d\4∀~∀~(~∀@@A!+ ↓βGiSYSir@4ZA a!K[Ke¬XACf↓oKYX↓CfA∪9KMMC YJ~∀4∃≠sgQKerA9k[EKH@dASLAoQr↓iQJ@ ISII1KHDAQ '(AIk\A←8As←kHA[CG!S]JA!Cf~∃∧@E[←⊃JDA←_@db`↓π!*AMKG←]⊃fACf↓←aa←MKHAi<ACE←Uh@bhLAπ!*↓gKG←9IfA←8AB~∃
←[aCICEYr5GY←G-KHA[¬GQS]∀AQKe∀Aek]9S]NAQQJAGUeeK]PAπ∨≥ %∪≡AIKYKCMJ\~∀!)QSf↓oCfA5rA[K¬gkeK5K]hA→←dAi!J@EI%IIYK⊂DAmKIgS←\ZZAs=jAeKA←eiK⊂@dnp~∃M←HAiQJ↓←eSO%]CXAYKegS=\AC]⊂A∩Ae∃G←eI∃H@drd\AM←HAiQJ↓←eSO%]CXAYKegS=\@ZZ↓Ekh@4∃iQJEISI⊃YKHD↓mKeg%←\ASL@UKq¬GiYr(AiQJ↓gC[J↓MSYJ↓∩AQC⊂AChAAβ%εX↓S\Ai!JAgC5J~∃e∃YKCg∀A←LA1Sg`R8@@@~(~∃∪h≥fACY5←ghA¬fASL↓s←jA!CHAg=[JAY¬eOJA=mKeQ∃CHAC
iSmSQrAO←%]NA←8ACYX↓iQJAQS[JX~∃gk
PACf↓g]Ce→S]NAU`AeC9I←ZAA+!fA¬]HAi!e←oS9NAiQ∃ZACo¬r\@AAk`AC
iSmSQr@~∃
←kYH↓EJAB↓QSOQ1r[mCISCEY∀AiQS9NXAC9HAG←UYHAC
G←k]PAM←d↓YCeO∀AiS[%]N@~)ISMM∃eK]G∃fAEKQoKK\↓gCrA→eSICdACMi∃e]←←8AC]H↓)QkeMICrA5←e]S9N\@~(~∃+]→←eik9CiKYdXASiLACYg<Ag←[∃iQS]≤AiQCPASfA9←hAK¬gSYr↓G←]iI←YYK⊂AErA∧AkgKH@~∃I=S]NAQS[S]≥fXAg%]GJA%hAIKAK]If↓iQJAA+ AC
iSmSQrA←L↓←iQKIfAkg∃efA←_AiQJ~∃gC5JAKi!Ke]KP\@@A
keeK9iYrX↓iS[J↓gaK]PAS\A%]iKe1Sg`[⊂@EIe=aaS]≤DA]←8Z~∃S9iK]I∃HA!+AfASf↓]←hAYSgSE1JAS\↓iQJAQS[S]≥fAgi¬iSgi%Gf@Q%hAo←UYHA[∃eKYr4∃EY←¬hAeKA←eiK⊂Aπ!*↓iS[J$\@A!U ACGQSmSidAG←k1HAEJ↓[←]SQ←eKH↓ErAC9←iQKH@~∃ =YaQS8Aek]9S]NA∃iQKe]CiGP↓oQSY∀As←j↓CeJAIk]]S9NAiS5S]Of↓←\As=kef\4∃7αAMS[aY∀AoCr↓←LAi∃[a←e¬eSYr↓ike]%]NA←→LA!+@ACGi%mSir↓[SOQPAQKY@~∃MS1iKdA=khAi!SfACLABAg=keGJ↓←LAm¬eSCE%YSirlACeJ↓s←jA%]iKe∃giKH↓S\AiIsS]N⎇:~∀~(~∀@@A/QCPAiQJ↓
Cgi∃dAπY=GVA←8AEksL@~∀~)≠rA =YaQS8ASfA%]IKK⊂AMCgQKdAi!C\A[¬]rA←QQKef0AEKG¬kgJA%hAQCLABAG1←GV@4∃GesMiCXAIk]]S9NAChhh\j↓≠KOC!Keit8@A)Q∀A ←YAQS\A]CfA←ISOS]¬YYrA%]iK]⊃KH~∃Q↑Aek8ACh@Ta≠⊃t0AEkh↓IkJAQ↑ABA1CeOKH[iQC8[Kqa∃GiKH↓mCeS¬ESYSQrAS\↓iQJ~)G←[a=]K]iL@QGQ%afXA∃iFRAQQJAaI←IkGQS←\A5←IKYLACeJ↓Gkee∃]iYr↓aKOO∃HACh4∀ha≠!t\@A5CGQS9KfAo%iPABhh\k5⊃tAG1←GVA!CmJA∧AgaK∃HAS]
eKCg∀A←LA¬E←khbdJAQ↑@~∀DlJ\@↓)QJAIKCg←8AoQr↓iQSf↓Sg\OPA[Ke∃Yr@b@JASf↓iQCh↓iQKe∀ASfA∧@EEk→MKeS9ND@~)CGiS=\A←L↓iQJA
←]gi¬]h[i%[JA←YKeQK¬HAeKEkSeK⊂AM←d↓[CS]QCS]S9NAiQ∀AISgAYCr~)C]HAMC[aY%]NAi!JAWKeE←Ce⊂vAiQUfABA→CgiKHA[CG!S]JAMaK]ILAae←A←eiS=]CiK1r~∃Y∃gfA←_ASif↓iS[J↓S\Ai!KgJA
←]gi¬]hA←YKeQK¬HAiCMWf\A=LAG←UegJXja≠⊃hAGY←
Wf~∃]←kYH↓eKgk1hAS\↓KmK\↓[←eJ↓aKeM=e[C]
JAS[Ae←mK5K]h\4∀~∀~(@@@A]QChA⊃∪'!→¬3 ∨/8AEksL~∀~∃$AiQ←UOQhAQQChAe←jAQ¬HAek8AoSi A ∪'A→β3 =/≤AIUeS]N↓iQJA
←[akQJZ~∃ ←k]H↓) '(lAg↑A$AeC\↓iQSf↓oCrA=\A[r↓ek]f0AKqG∃ahAM=dAiQ=gJAS9iK]I∃H@~∃Q↑AOCQQKdA⊃CiBA]QSGP↓o←kY⊂AG←eIKYCi∀AiQJ↓KMMK
hA←L↓ ∪'!1β3 ∨]≤\~∃%hA[C-KfAg∃]gJAQ↑AI↑↓g↑A←8@UG←5akiJ5E←k]⊂TAiCMWfXAMS]GJ↓C\ACYKeCO∀@~∃gAKKHA%]GeK¬gJA←_@hbJ↓i↑@hTJASf↓iQKe∃ErA← iCS]∃H\@@4∀~∃βLAKqa∃GiKH0AiQJ↓ISga1CrA←→LA[K¬]fA[=eJAi<Aπ!*↓iS[J↓←\ABha≠⊃h@~∃[¬GQS]∀AiQC8Ai↑AQQChA=\AB@Ph\k≠!tA←]∀@ZZ@PfJACLA←aa=gKHAQ↑A←]1r@fl∀\~∃∂ AiS[%]OfA¬eJAg<AmCe%CEYJ↓iQCh↓∩AMC
i←eK⊂AiQK4A←kh↓M←dAQQKgJ↓aKeG∃]iCO∃f\~∀4∃7∩A⊃←\Oh↓iQS],A←]J↓o←kY⊂AgKJ↓C]si!S]NA1SWJAQQSfA≥CS\A%LAiQ∀AWKs ←CeH~∃gC5aYS]≤A[K]QS←]K⊂ACE←YJAoKIJAgS5SYCe1rAgQUhA←M_vA ←ICI↑AM)β)&↓a←S]P@~∃i<A[Cs J@lJ↓a←gg%EYJX↓EkhA∃mK\AQQSfA=mKeQ∃CHAG=ghA[¬rAO↑↓I←o\↓CfA[=eJ~∃M←Mio¬eJASLAIKm∃Y←aK⊂\@@A¬fABAMSIJA
←[[K9hXAI%gaYCdA[CS9iK]C9GJASLA]←h~∃BAMSO]S→SGC]PAMCGQ←dAS8AiQJ↓ ←eC⊃↑A←d∂\Ai!JA C9IK→S=\]:~(~∀~∀@@A/!ChAs=jAGC8A qa∃GhAM=dA ←1aQS\↓'aKK⊂A∪]GIKCgKLA'←←8~∀~∃QQJA/%≥λAm∃egS←8A←LAQQJAg=MioCIJ@Ao%YXAY%WKYr↓EJAe∃YKCg∃HAYCQKdAi!Sf~∃eKCdX↓C]HAQQJAI¬iBAQ∃eKS\↓S]IS
CiJA∧A[S]%[kZA=LACE=kh@b@JA←m∃eCYX~∃S]
eKCg∀AS\AMaKKHl@A←i!KdAaIKYS[%]Cer↓[KCgUeKfAMkOOKMhABAMaKKH5k`A←_~∀bj∀Ai↑@H`J\@↓
Cgi∃dAQCIIoCe∀A[Cr↓EJAS8AiQJ↓o←eWLXAEkPA∩OZ↓]←hAQQJA←9J~∃i<AG←[5K]hA%\AC]dA←MM%GCXA]CrAC ←khAQQSf\ Maybe when we get some
more benchmarks (such as Dick Gabriel is pushing for), we'll do them
on the latest Dolphins.
Just for the record, I'd like to include some timings given me by Larry,
which were done on the Dolphin of one year ago (the "diddled" version
of the problem):
Swap time = 30secs
GC time = 175secs
CPU time = 750secs
Elapsed = 950secs
So today's "vanilla" times are 5.6 times faster than last years, and on my
44.5Mhz machine running WIND I see a speed-up of a factor of 7.
A factor of 7!
Bill van Melle suggests that these speed-ups are due mainly to improvements
in function call and CONS, and that's precisely what the Boyer-Moore
IREWRITE benchmark tests. I really don't think anything quite that dramatic is
on the horizon for the *overall* Dolphin performance, but *selected areas*
which we have targeted for more devolpment could show stellar improvement.
(such as putting floating-point into microcode).
Hope to see you at AAAI.
_________________________________________________
The Raw Data
Machines: GSN (Gordon Novak's), JONL (mine), SYBAL (John Sybalsky's)
[GSN and SYBAL have 40MHz, JONL has 44.5MHz]
Finisterra (the only Dorado included)
Program: OB (Old Boyer code, without declarations)
NB (New Boyer code, with GLOBALVARS for free temps)
Diddled (Larry Masinter's reworking using local lambda
binding for temporaries)
Version: CB (current release CONBRIO), WD (WIND system)
Options: DD (display "down", or off), DU (display "up")
1st (first run), nth ("mode", or most frequently observed after first)
All measurements in seconds. Timings on SYBAL,NB,CB,DD were also
reproduced quite closely on Larry Masinter's machine, and on Stu Card's.
Display Up vs. Display Down times
-----------------------------------------------------------------
Swap 3.6 GSN | Swap 3.0 GSN July 2
GC 66.4 OB | GC 49. OB
CPU 415. CB,DU,nth | CPU 299. CB,DD,nth
Swap 33.1 GSN | Swap 5.7 GSN July 2
GC 70.0 diddled | GC 50.9 diddled
CPU 305. CB,DU,1st | CPU 210. CB,DD,nth
Swap 0.5 JONL | Swap - JONL July 2
GC 60. diddled | GC 30.2 diddled
CPU 158. WD,DU,nth | CPU 116. WD,DD,nth
Swap - SYBAL | Swap - SYBAL July 7
GC 56. diddled | GC 39.6 diddled
CPU 204. CB,DU,nth | CPU 143. CB,DD,nth
First run vs. nth ("mode") run; Display Down
-----------------------------------------------------------------
Swap 2. JONL | Swap - JONL July 7
GC 26.7 NB | GC 31.6 NB
CPU 142. CB,DD,1st | CPU 117. CB,DD,nth
Swap .2 JONL | Swap - JONL July 7
GC 24.9 NB | GC 28.2 NB
CPU 119. WD,DD,1st | CPU 107. WD,DD,nth
Swap 9.8 SYBAL | Swap - SYBAL July 7
GC 31. NB | GC 35. NB
CPU 140. CB,DD,1st | CPU 132. CB,DD,nth
Swap .14 SYBAL | Swap - SYBAL July 7
GC 20.6 NB | GC 31.7 NB
CPU 133. WD,DD,1st | CPU 119. WD,DD,nth
Swap .1 SYBAL | Swap - SYBAL July 7
GC 33.2 diddled | GC 35. diddled
CPU 150. WD,DD,1st | CPU 130. WD,DD,nth
Dorado time
-----------------------------------------------------------------
Swap ? Finisterra | Swap - Finisterra July 2
GC 11.4 diddled | GC 17. diddled
CPU 25.6 WD,1st | CPU 22.7 WD,nth
The STATS file mentioned for Dorado analysis is on the PHYLUM
file server at PARC, file <JONL>TEST.PRINTOUT. Since it's a
lengthy account of an incomplete run, I didn't reproduce it here.
Mail-from: ARPANET site SU-SCORE rcvd at 8-Jul-82 1245-CDT
Date: 8 Jul 1982 1043-PDT
From: Gordon Novak <CSD.NOVAK at SU-SCORE>
To: Masinter at PARC-MAXC, CL.BOYER at UTEXAS-20
cc: JonL at PARC-MAXC
In-Reply-To: Your message of 7-Jul-82 1812-PDT
Date: Thursday, 8 July 1982 12:43-CDT
From: Gordon Novak <CSD.NOVAK at SU-SCORE>
To: Masinter at PARC-MAXC, CL.BOYER
cc: JonL at PARC-MAXC
I reran the test as Larry did, with similar results (included below).
My problem was that I used TCOMPL instead of BCOMPL. I recall being
told by someone that the Dolphin didn't block-compile like Interlisp-10,
so that BCOMPL and TCOMPL did the same thing. Obviously that isn't true;
I should have been more careful. I apologize for raising a ruckus over
a silly mistake; at least I'm glad that the results will be fair to the
Dolphin crowd.
DISPLAYDOWN, as used in Larry's test, totally turns off the display for
the duration. I haven't used it myself, but I understand that it can
get one into funny problemsif e.g. there are errors in the execution
of the program with the display off; I don't know if most users would
find it acceptable to run in this mode.
NIL
Mail-from: ARPANET site PARC-MAXC rcvd at 13-Jul-82 0217-CDT
From: JonL at PARC-MAXC
To: CL.BOYER
cc: JonL at PARC-MAXC
Re: Timings Table for IREWRITE benchmark
Yes, the SYBAL,NB,CB,DD is an appropriate time for the current "vanilla"
Dolphin; but the Dorado timing I reported in the previous note can't be
strictly compared with the others since it was running the "diddled" test
rather than the NewBoyer (NB) test, and was in the WIND release rather
than CONBRIO. [As it happens, the "diddling" had somewhat of a misfeature
in it, which is why I mentioned that NB is a much better benchmark anyway].
Dorado Frontenac, NewBoyer.benchmark(NB),systemCONBRIO(CB)
DisplayDown (DD) times for "mode" (nth) run:
GC = 10.9
CPU = 17.6
DisplayUp (DU) times for "mode" (nth) run:
GC = 11.8
CPU = 19.2
DisplayDown (DD) times for "FirstRun" (1st) run:
Swap = .027
GC = 10.5
CPU = 17.4
It's not clear to me why the "FirstRun" time was faster in these trials -- chalk
it up to "noise", or maybe to the benefits of larger-memory/faster-disk?
∨
←LOAD(IREWRITE.DCOM)
compiled on 8-JUL-82 09:54:44
FILE CREATED 5-Jul-82 12:52:49
IREWRITECOMS
{DSK}IREWRITE.DCOM;2
←(DISPLAYDOWN (TIMEALL (SETUP)))
Elapsed Time = .755 seconds
SWAP time = .582 seconds
CPU Time = .173 seconds
PAGEFAULTS = 12
LISTP
224
T
←(DISPLAYDOWN '(TIMEALL (TEST)))
Elapsed Time = 175.0 seconds
SWAP time = 6.63 seconds
GC time = 31.5 seconds
CPU Time = 137.0 seconds
PAGEFAULTS = 610
SWAPWRITES = 157
FIXP LISTP
311 226469
(T 168388 31471)
←REDO
Elapsed Time = 183.0 seconds
SWAP time = .494 seconds
GC time = 48.7 seconds
CPU Time = 134.0 seconds
PAGEFAULTS = 21
FIXP LISTP
375 226469
(T 182913 48703)
←REDO
Elapsed Time = 188.0 seconds
SWAP time = .078 seconds
GC time = 52.3 seconds
CPU Time = 136.0 seconds
PAGEFAULTS = 2
FIXP LISTP
419 226469
(T 188209 52257)
←REDO
Elapsed Time = 188.0 seconds
SWAP time = .015 seconds
GC time = 51.2 seconds
CPU Time = 137.0 seconds
PAGEFAULTS = 14
FIXP LISTP
401 226469
(T 187906 51188)
←TIMEALL((TEST))
Elapsed Time = 271.0 seconds
SWAP time = .059 seconds
GC time = 75.3 seconds
CPU Time = 195.0 seconds
PAGEFAULTS = 1
FIXP LISTP
420 226469
(T 270715 75315)
←TIMEALL((TEST))
Elapsed Time = 267.0 seconds
SWAP time = .006 seconds
GC time = 73.2 seconds
CPU Time = 194.0 seconds
PAGEFAULTS = 6
FIXP LISTP
402 226469
(T 267145 73153)
←TIMEALL((TEST))
Elapsed Time = 266.0 seconds
GC time = 72.6 seconds
CPU Time = 194.0 seconds
FIXP LISTP
402 226469
(T 266215 72623)
←DRIBBLE]
∨
The INTERLISP VAX test
Mail-from: ARPANET site USC-ISIB rcvd at 23-Jul-82 1108-CDT
Date: 23 Jul 1982 0907-PDT
Sender: RBATES at USC-ISIB
Subject: Re: lisp comparison.
From: Raymond Bates <RBATES at ISIB>
To: CL.BOYER at UTEXAS-20
Cc: CMP.GOOD at UTEXAS-20, ddyer at USC-ISIB, lynch at USC-ISIB,
Cc: Novak at SUMEX-AIM
Message-ID: <[USC-ISIB]23-Jul-82 09:07:07.RBATES>
In-Reply-To: Your message of Thursday, 22 July 1982 13:12-CDT
*** EOOH ***
Date: Friday, 23 July 1982 11:07-CDT
From: Raymond Bates <RBATES at ISIB>
Sender: RBATES at USC-ISIB
To: CL.BOYER
cc: CMP.GOOD, ddyer at USC-ISIB, lynch at USC-ISIB, Novak at SUMEX-AIM
Re: lisp comparison.
Here is the DRIBBLE file of a long run:
NIL
4←(GCGAG NIL]
40
5←LOAD(IREWRITE.v]
compiled on 22-JUL-82 09:22:17
File Created: 5-Jul-82 12:52:49
% warning! this file possibly incompatible!
Compiled by version 3.0 but current version is 2.1
IREWRITECOMS
/lisp/rbates/lisp/IREWRITE.v;2
6←(SETUP]
T
7←(FOR I FROM 1 TO 20 DO (PRINT (TEST ]
(T 76048 0)
(T 76464 0)
(T 76496 0)
(T 76272 0)
(T 89072 4784)
(T 80992 0)
(T 81840 0)
(T 81600 0)
(T 90512 4752)
(T 81904 0)
(T 82032 0)
(T 81248 0)
(T 90512 5456)
(T 80768 0)
(T 80800 0)
(T 80656 0)
(T 91424 5456)
(T 82112 0)
(T 82384 0)
(T 82432 0)
NIL
8←(DRIBBLE]
You many wonder why the cpu time has an extra 10 seconds each
time the system does a gc. The reason is that the system has to
re-hash all the hash array after the gc and time is being charge
to the computation time and not gc time (we will fix that). This
test was done on our 780. Any thing else you would like to see
or known?
/Ray
∨
;;; SAIL
(fasload boyer)
(timit)
Timing performed on Wednesday 09/15/82 at 10:50:58.
Cpu Time = 7.635
Elapsed Time = 726.53333
Wholine Time = 241.866667
GC Time = 120.472
Load Average Before = 6.1742424
Load Average After = 2.85985446
Average Load Average = 4.5170484
NIL
Timing performed on Wednesday 09/15/82 at 11:03:27.
Cpu Time = 7.49
Elapsed Time = 65.0
Wholine Time = 36.4166665
GC Time = 12.669
Load Average Before = 2.54934967
Load Average After = 2.2733817
Average Load Average = 2.4113657
NIL
Timing performed on Wednesday 09/15/82 at 11:04:44.
Cpu Time = 7.509
Elapsed Time = 59.3166666
Wholine Time = 32.866667
GC Time = 11.513
Load Average Before = 2.17366004
Load Average After = 2.06962526
Average Load Average = 2.12164265
NIL
;;; SAIL (FIXSW T)
(fasload boyer)
(timit)
Timing performed on Wednesday 09/15/82 at 11:06:16.
Cpu Time = 7.629
Elapsed Time = 1076.21666
Wholine Time = 229.366667
GC Time = 120.4
Load Average Before = 1.81269705
Load Average After = 8.4301555
Average Load Average = 5.1214263
NIL
Timing performed on Wednesday 09/15/82 at 11:24:17.
Cpu Time = 7.494
Elapsed Time = 86.016666
Wholine Time = 36.733333
GC Time = 12.692
Load Average Before = 8.2354884
Load Average After = 5.64889336
Average Load Average = 6.9421909
NIL
Timing performed on Wednesday 09/15/82 at 11:25:45.
Cpu Time = 7.484
Elapsed Time = 82.3
Wholine Time = 33.983333
GC Time = 11.519
Load Average Before = 5.58177483
Load Average After = 4.12152493
Average Load Average = 4.8516499
NIL
;;; Boyer
D2
7/5/83
Without interrupts
SETUP:
Elapsed .839
Swap .732
CPU .107
pgflts 21
dskops 18
TEST:
Elapsed 132.0
GC 31.3
CPU 101.0
pgflts 554
swpwrts 76
dskops 76
D3
7/5/83
with interrupts, jonl env
SETUP:
Elapsed .034
Swap .014
CPU .02
pgflts 3
TEST:
Elapsed 44.0
GC 17.0
pgflts 520
swpwrts 113
dskops 113
with interrupts, bare env
TEST:
Elapsed 30.3
GC 13.2
CPU 17.1
pgflts 2
;;; NIL
;;; Friday July 22,1983 2:16 FQ+4D.16H.41M.10S. -*- Text -*-
BOYER
Pass 1. Changes to preserve semantics:
(member x y) => (member x y :test #'equal)
try 1:
cpu=116.5, elapsed=119.9, pagefaults=3907
Try 2:
cpu=115.76, elapsed=120.70, pagefaults=3961
Note... I ran this part several times while experimenting with
getting VMS to let me have the machine to myself (and not play musical
pages with me). As i have noticed before, the times vary; in this
case, from as little as 114 seconds (surprisingly, on one which paged
more), to the 120 here (again surprisingly, which was set to page less).
----------------
Pass 2. Change, in TRANS-OF-IMPLIES1, (EQUAL N 1) -> (EQL N 1).
Turn ON open-compilation of CAR, CDR, RPLACA, etc.
Try 1:
cpu=81.33,elapsed=83.78,pagefaults=3965
Try 2:
cpu=81.69,elapsed=85.11,pagefaults=3993
----
Comments. Heavy on function calls; this will show in NIL.
Probably heavy on use of EQUAL. The NIL EQUAL function leaves
much to be desired in efficiency (partly from function calls),
especially in the simple cases. EQUAL is probably going to be
written in macro-32 soon, to handle the simple cases.
;;; FRANZ
∂06-Jun-83 1039 RPG boyer
∂01-Jun-83 2251 jkf%UCBKIM@Berkeley boyer
Received: from UCB-VAX by SU-AI with TCP/SMTP; 1 Jun 83 22:45:09 PDT
Date: 1 Jun 83 22:46:28 PDT (Wed)
From: jkf%UCBKIM@Berkeley (John Foderaro)
Subject: boyer
Message-Id: <8306020546.13350@UCBKIM.ARPA>
Received: by UCBKIM.ARPA (3.340/3.5)
id AA13350; 1 Jun 83 22:46:28 PDT (Wed)
Received: from UCBKIM.ARPA by UCBVAX.ARPA (3.341/3.31)
id AA10232; 1 Jun 83 22:45:39 PDT (Wed)
To: rpg@su-ai
(780cpu,gc)/(750cpu,gc) [seconds]
>>> boyer: test
translinks
on off
localf 21.33,50.42/36.18,82.35 21.3,21.32/36.15,35.01
compiled 40.13,50.43/62.38,78.68 137.85,21.25/223.47,34.5
interpreted 1061.02,32.25/1699.95,51.77 1058.88,22.47/1685.92,36.73
**** New Franz
∂09-Oct-83 0937 jkf@ucbkim boyer
Received: from UCBKIM by SU-AI with TCP/SMTP; 9 Oct 83 09:37:37 PDT
Received: by ucbkim.ARPA (4.6/4.2)
id AA17661; Sun, 9 Oct 83 09:41:06 PDT
Date: Sun, 9 Oct 83 09:41:06 PDT
From: John Foderaro (on an h19-u) <jkf@ucbkim>
Message-Id: <8310091641.AA17661@ucbkim.ARPA>
To: rpg@su-ai
Subject: boyer
Cc:
--- Benchmark boyer run on ucbkim at Sat Oct 8 02:45:06 PDT 1983 by jkf
--- cpu usage: 2:45am up 3:15, 0 users, load average: 1.12, 1.13, 1.15
Franz Lisp, Opus 38.81
=> [fasl boyer.o]
t
=> benchmark: test (file boyer) , tranlinks: on, localf: no
executing form: (test)
begin (217 213)
end (4507 2093)
runs 1
avg cpu time 40.16666666666667, avg gc time 31.33333333333333
benchmark: test (file boyer) , tranlinks: off, localf: no
executing form: (test)
begin (4507 2093)
end (14485 3372)
runs 1
avg cpu time 144.9833333333333, avg gc time 21.31666666666667
nil
=> Franz Lisp, Opus 38.81
=> [fasl boyer-l.o]
t
=> benchmark: test (file boyer) , tranlinks: on, localf: yes
executing form: (test)
begin (208 211)
end (3308 2076)
runs 1
avg cpu time 20.58333333333333, avg gc time 31.08333333333333
benchmark: test (file boyer) , tranlinks: off, localf: yes
executing form: (test)
begin (3310 2076)
end (5851 3357)
runs 1
avg cpu time 21.0, avg gc time 21.35
nil
=> Franz Lisp, Opus 38.81
=> [load boyer.l]
[fasl benchmac.o]
[fasl benchmac.o]
t
=> benchmark: test (file boyer) , tranlinks: on, interpreted
executing form: (test)
begin (304 247)
end (63663 2112)
runs 1
avg cpu time 1024.9, avg gc time 31.08333333333333
benchmark: test (file boyer) , tranlinks: off, interpreted
executing form: (test)
begin (63665 2112)
end (126963 3672)
runs 1
avg cpu time 1028.966666666667, avg gc time 26.0
nil
=> --- cpu usage: 3:29am up 3:59, 0 users, load average: 1.31, 1.14, 1.12
--- end of benchmark boyer
--- Benchmark boyer run on ucbmatisse at Fri Oct 7 18:16:45 PDT 1983 by jkf
--- cpu usage: 6:16pm up 2:46, 1 users, load average: 1.21, 0.50, 0.29
Franz Lisp, Opus 38.81
=> [fasl boyer.o]
t
=> benchmark: test (file boyer) , tranlinks: on, localf: no
executing form: (test)
begin (400 273)
end (7087 3327)
runs 1
avg cpu time 60.55, avg gc time 50.9
benchmark: test (file boyer) , tranlinks: off, localf: no
executing form: (test)
begin (7089 3327)
end (22613 5409)
runs 1
avg cpu time 224.0333333333333, avg gc time 34.7
nil
=> Franz Lisp, Opus 38.81
=> [fasl boyer-l.o]
t
=> benchmark: test (file boyer) , tranlinks: on, localf: yes
executing form: (test)
begin (385 268)
end (5505 3327)
runs 1
avg cpu time 34.35, avg gc time 50.98333333333333
benchmark: test (file boyer) , tranlinks: off, localf: yes
executing form: (test)
begin (5507 3327)
end (9689 5429)
runs 1
avg cpu time 34.66666666666667, avg gc time 35.03333333333333
nil
=> Franz Lisp, Opus 38.81
=> [load boyer.l]
[fasl benchmac.o]
[fasl benchmac.o]
t
=> benchmark: test (file boyer) , tranlinks: on, interpreted
executing form: (test)
begin (486 273)
end (99686 3314)
runs 1
avg cpu time 1602.65, avg gc time 50.68333333333333
benchmark: test (file boyer) , tranlinks: off, interpreted
executing form: (test)
begin (99691 3314)
end (197940 5422)
runs 1
avg cpu time 1602.35, avg gc time 35.13333333333333
nil
=> --- cpu usage: 7:24pm up 3:54, 0 users, load average: 1.00, 1.03, 1.04
--- end of benchmark boyer
--- Benchmark boyer run on ucbmike at Fri Oct 7 14:40:16 PDT 1983 by jkf
--- cpu usage: 2:40pm up 5:12, 0 users, load average: 1.14, 1.05, 1.04
Franz Lisp, Opus 38.79
-> [fasl boyer.o]
t
-> benchmark: test (file boyer) , tranlinks: on, localf: no
executing form: (test)
begin (469 450)
end (8861 4979)
runs 1
avg cpu time 64.38333333333334, avg gc time 75.48333333333333
benchmark: test (file boyer) , tranlinks: off, localf: no
executing form: (test)
begin (8866 4979)
end (26752 8086)
runs 1
avg cpu time 246.3166666666667, avg gc time 51.78333333333333
nil
-> Franz Lisp, Opus 38.79
-> [fasl boyer-l.o]
t
-> benchmark: test (file boyer) , tranlinks: on, localf: yes
executing form: (test)
begin (458 441)
end (7517 4963)
runs 1
avg cpu time 42.28333333333333, avg gc time 75.36666666666666
benchmark: test (file boyer) , tranlinks: off, localf: yes
executing form: (test)
begin (7522 4963)
end (13188 8058)
runs 1
avg cpu time 42.85, avg gc time 51.58333333333334
nil
-> Franz Lisp, Opus 38.79
-> [load boyer.l]
[fasl benchmac.o]
[fasl benchmac.o]
t
-> benchmark: test (file boyer) , tranlinks: on, interpreted
executing form: (test)
begin (651 510)
end (118177 5034)
runs 1
avg cpu time 1883.366666666667, avg gc time 75.40000000000001
benchmark: test (file boyer) , tranlinks: off, interpreted
executing form: (test)
begin (118185 5034)
end (234299 8116)
runs 1
avg cpu time 1883.866666666667, avg gc time 51.36666666666667
nil
-> --- cpu usage: 4:04pm up 6:35, 0 users, load average: 1.10, 1.06, 1.03
--- end of benchmark boyer
;;; SCORE Oct 18, 1983
LISP
LOAD(BOYER)
MAKEFILE(BOYER)
CLEANUP)
BCOMPL(BOYER)
ST
(SETUP)
(TIME (TEST) 1 3)
(TIME (TEST) 1 3)
collecting lists
8974, 10510 free cells
collecting lists
9127, 10151 free cells
collecting lists
9346, 10370 free cells
collecting lists
1655, 10359 free cells
collecting lists
2054, 10246 free cells
collecting lists
7526, 10086 free cells
collecting lists
7204, 10276 free cells
collecting lists
7256, 10328 free cells
collecting lists
9076, 10100 free cells
collecting lists
6754, 10338 free cells
collecting lists
7772, 10332 free cells
collecting lists
7768, 10328 free cells
collecting lists
6910, 10494 free cells
collecting lists
7584, 10144 free cells
collecting lists
8692, 10228 free cells
collecting lists
7188, 10260 free cells
collecting lists
11498, 11498 free cells
collecting lists
8254, 10302 free cells
collecting lists
7180, 10252 free cells, 36 pages left
collecting lists
7254, 10326 free cells, 30 pages left
collecting lists
8952, 10488 free cells, 27 pages left
collecting lists
8470, 10006 free cells, 24 pages left
226469 conses
25.458 seconds
27.479 seconds, garbage collection time
(T 52933 27479)
←